(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))

(def-constant rad%dist"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 (instantiate-existential ("rad%dist(a_0)")) (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 (instantiate-existential ("rad%dist(a_0)")) (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)"))

(def-theorem bounded-rad-dist"forall(n:ind_1,x:bfun, dist(a_0,x(n))<=sup(ran{rad%dist oo x}))"(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 (unfold-single-defined-constant (0) rad%dist) (instantiate-existential ("n")) simplify (backchain"forall(x:[ind_1,pp],#(x,bfun) iff (total_q{x,[ind_1,pp]} and #(sup(ran{rad%dist oo x}))))"))) (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) (instantiate-existential ("sup(ran{rad%dist oo x_0})+sup(ran{rad%dist oo x_1})")) (apply-macete-with-minor-premises sum-inequality-macete) (instantiate-existential ("a_0")) (apply-macete-with-minor-premises symmetry-of-distance) (apply-macete-with-minor-premises bounded-rad-dist) (apply-macete-with-minor-premises bounded-rad-dist))) (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 (instantiate-existential ("sup(ran{rad%dist oo x})+sup(ran{rad%dist oo y})")) (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) (apply-macete-with-minor-premises bounded-rad-dist) (apply-macete-with-minor-premises bounded-rad-dist))) (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)))