```(def-language pointed-metric-spaces
(embedded-languages metric-spaces-language)
(constants (a_0 pp)))

```

```
(def-theory pointed-metric-spaces
(component-theories metric-spaces)
(language pointed-metric-spaces))
```

```
(def-theory mappings-into-a-pointed-metric-space
(component-theories pointed-metric-spaces generic-theory-1))
```

```
"lambda(x:pp, dist(a_0,x))"
(theory pointed-metric-spaces))
```

```(def-theorem ()
"lambda(f:[ind_1,pp], total_q{f,[ind_1,pp]} and #(sup(ran{rad%dist oo f})))(lambda(x:ind_1, a_0))"
(proof
(beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
insistent-direct-inference
beta-reduce-repeatedly ;;gr
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-with-minor-premises
beta-reduce-with-minor-premises
beta-reduce-with-minor-premises
(instantiate-existential ("x_\$1"))
simplify
unfold-defined-constants
(apply-macete-with-minor-premises tr%prec%majorizes%characterization)
direct-and-antecedent-inference-strategy
beta-reduce-repeatedly
simplify))
(theory mappings-into-a-pointed-metric-space))

```

```
(def-atomic-sort bfun
"lambda(f:[ind_1,pp], total_q{f,[ind_1,pp]} and #(sup(ran{rad%dist oo f})))"
(theory mappings-into-a-pointed-metric-space)
(witness "lambda(x:ind_1, a_0)"))
```

```

(proof
((assume-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(instantiate-existential ("dist(a_0,x(n))"))
simplify-insistently
(instantiate-existential ("n"))
simplify
(backchain "forall(x:[ind_1,pp],#(x,bfun)
iff
(theory mappings-into-a-pointed-metric-space))
```

```
(def-constant bfun%dist
"lambda(f,g:bfun, sup(ran{lambda(x:ind_1, dist(f(x),g(x)))}))"
(theory mappings-into-a-pointed-metric-space))
```

```(def-theorem ()
"total_q{bfun%dist,[bfun,bfun,rr]}"
lemma
(proof
((assume-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space)
insistent-direct-inference
(unfold-single-defined-constant (0) bfun%dist)
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%non-empty-range)
beta-reduce-repeatedly
(instantiate-existential ("x_\$0"))
simplify
(apply-macete-with-minor-premises tr%prec%majorizes%characterization)
beta-reduce-repeatedly
(apply-macete-with-minor-premises triangle-inequality-alternate-form)
(apply-macete-with-minor-premises sum-inequality-macete)
(instantiate-existential ("a_0"))
(apply-macete-with-minor-premises symmetry-of-distance)
(usages d-r-convergence)
(theory mappings-into-a-pointed-metric-space))
```

```
(def-theorem bounded-bfun%dist
"forall(x,y:bfun,n:ind_1 ,dist(x(n),y(n))<=bfun%dist(x,y))"
(proof
((assume-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space)
(unfold-single-defined-constant (0) bfun%dist)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(instantiate-existential ("dist(x(n),y(n))"))
simplify-insistently (instantiate-existential ("n"))
simplify (apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%non-empty-range)
beta-reduce-repeatedly simplify
(apply-macete-with-minor-premises tr%prec%majorizes%characterization)
beta-reduce-repeatedly
(apply-macete-with-minor-premises triangle-inequality-alternate-form)
(instantiate-existential ("a_0"))
(apply-macete-with-minor-premises sum-inequality-macete)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises symmetry-of-distance)
(usages transportable-macete)
(theory  mappings-into-a-pointed-metric-space))

```

```(def-theorem ()
"forall(x,y,z:bfun, bfun%dist(x,z)<=bfun%dist(x,y)+bfun%dist(y,z))"
lemma
(proof
((unfold-single-defined-constant (0) bfun%dist)
(apply-macete-with-minor-premises tr%lub-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%prec%majorizes%characterization)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises triangle-inequality-alternate-form)
(instantiate-existential ("y(n_\$0)"))
(apply-macete-with-minor-premises sum-inequality-macete)
(apply-macete-with-minor-premises bounded-bfun%dist)
(assume-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space)
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%non-empty-range)
beta-reduce-repeatedly
(assume-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space)
simplify
auto-instantiate-existential))
(theory  mappings-into-a-pointed-metric-space))
```

```(def-theorem ()
"forall(x,y:bfun, bfun%dist(x,y)=bfun%dist(y,x))"
(proof
((unfold-single-defined-constant (0 1) bfun%dist)
(apply-macete-locally symmetry-of-distance (0) " dist(x(x_\$0),y(x_\$0)) ")
simplify
(assume-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space)
(cut-with-single-formula "total_q{bfun%dist,[bfun,bfun,rr]}")
(incorporate-antecedent "total_q{bfun%dist,[bfun,bfun,rr]}")
(unfold-single-defined-constant (0) bfun%dist)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "total_q{lambda(f,g:bfun,
sup(ran{lambda(x:ind_1,dist(f(x),g(x)))})),[bfun,bfun,rr]}"
("y" "x"))
(beta-reduce-antecedent
"with(x,y:bfun,
#(lambda(f_\$0,g_\$0:bfun,
sup(ran{lambda(x_\$0:ind_1,dist(f_\$0(x_\$0),g_\$0(x_\$0)))})) (y,x)))")
insistent-direct-inference))
(theory  mappings-into-a-pointed-metric-space))
```

```(def-theorem ()
"forall(x,y:bfun, 0<=bfun%dist(x,y))"
(proof
(direct-and-antecedent-inference-strategy
(unfold-single-defined-constant (0) bfun%dist)
(apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(instantiate-existential ("dist(x(x_\$0),y(x_\$0))"))
(assume-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space)
simplify
(instantiate-existential ("x_\$0"))
simplify
(assume-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space)
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%non-empty-range)
beta-reduce-repeatedly
simplify
(apply-macete-with-minor-premises tr%prec%majorizes%characterization)
beta-reduce-repeatedly
(instantiate-existential ("bfun%dist(x,y)"))
(apply-macete-with-minor-premises bounded-bfun%dist)))
(theory  mappings-into-a-pointed-metric-space))
```

```(def-theorem ()
"forall(x,y:bfun, x=y iff bfun%dist(x,y)=0)"
(theory  mappings-into-a-pointed-metric-space)
(proof
((assume-theorem bfun-defining-axiom_mappings-into-a-pointed-metric-space)
direct-and-antecedent-inference-strategy
(force-substitution "y" "x" (0))
(weaken (0))
(unfold-single-defined-constant (0) bfun%dist)
(apply-macete-with-minor-premises zero-self-distance)
(weaken (0))
(cut-with-single-formula "forall(x,y:rr,x<=y and y<=x implies x=y)")
(backchain "forall(x,y:rr,x<=y and y<=x implies x=y);")
direct-and-antecedent-inference-strategy
(weaken (0))
(apply-macete-with-minor-premises tr%lub-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%prec%majorizes%characterization)
beta-reduce-repeatedly
simplify
(weaken (0))
(apply-macete-with-minor-premises tr%prec%sup-defined)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%non-empty-range)
beta-reduce-repeatedly
(weaken (0))
(instantiate-existential ("0"))
(weaken (0 1))
(apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup)
direct-and-antecedent-inference-strategy
(instantiate-existential ("0"))
simplify-insistently
(weaken (0))
simplify
extensionality
direct-and-antecedent-inference-strategy
(force-substitution "x(x_0)==y(x_0)" "dist(x(x_0),y(x_0))<=bfun%dist(x,y)" (0))
(apply-macete-with-minor-premises bounded-bfun%dist)
(force-substitution "x(x_0)==y(x_0)" "x(x_0)=y(x_0)" (0))
(apply-macete-with-minor-premises point-separation-for-distance)
direct-and-antecedent-inference-strategy
simplify
simplify)))
```