```(def-theory-ensemble-multiple metric-spaces 3)
```

```(def-theory-ensemble-instances metric-spaces
(permutations (0 1) (1 2) (0 2))
(target-multiple 3))
```

```(def-theory-ensemble-overloadings metric-spaces (1 2))
```

```
(def-theorem general-composition-of-continuous-functions
"forall(f:[pp_0,pp_1],g:[pp_1,pp_2],x:pp_0,continuous%at%point(f,x) and continuous%at%point(g,f(x)) implies continuous%at%point(g oo f,x))"
(theory metric-spaces-3-tuples)
(proof
(
unfold-defined-constants
beta-reduce-with-minor-premises
direct-and-antecedent-inference-strategy
(auto-instantiate-universal-antecedent "with(p:prop,forall(eps:rr,  0<eps implies p))")
(instantiate-universal-antecedent "with(p:prop,forall(eps:rr,  0<eps implies p))" ("delta_\$0"))
(instantiate-existential ("delta"))
(backchain "forall(y_\$0:pp_1,dist_1(f(x),y_\$0)<=delta_\$0
implies
dist_2(g(f(x)),g(y_\$0))<=eps_\$0)")
(backchain "forall(y:pp_0,
dist_0(x,y)<=delta implies dist_1(f(x),f(y))<=delta_\$0)")
(cut-with-single-formula "dist_1(f(x),f(y_\$0))<=delta_\$0")
(instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("1"))
(simplify-antecedent "not(0<1);")
(cut-with-single-formula "dist_1(f(x),f(x))<=1")
(backchain "forall(y:pp_0,dist_0(x,y)<=delta implies dist_1(f(x),f(y))<=1)")
(apply-macete-with-minor-premises tr%zero-self-distance)
simplify
)
(usages transportable-macete)))
```