```(def-language pointed-target-space
(embedded-languages metric-spaces-2-tuples)
(constants (a_0 pp_1)))
```

```
(def-theory pointed-ms-2-tuples
(language  pointed-target-space)
(component-theories  metric-spaces-2-tuples))
```

```
(def-translation mappings-pointed-metric-spaces-2-tuples
(source mappings-into-a-pointed-metric-space)
(target pointed-ms-2-tuples)
(sort-pairs (ind_1 pp_0) (pp pp_1))
(constant-pairs (a_0 a_0) (dist dist_1))
(fixed-theories h-o-real-arithmetic)
(theory-interpretation-check using-simplification))
```

```(def-transported-symbols (bfun%dist bfun)
(translation  mappings-pointed-metric-spaces-2-tuples)
(renamer mappings-to-pointed-target-space-renamer))
```

```(def-theorem ()
"forall(x,y,z:bfun, bfun%dist(x,z)<=bfun%dist(x,y)+bfun%dist(y,z))"
lemma
(home-theory mappings-into-a-pointed-metric-space)
(translation mappings-pointed-metric-spaces-2-tuples)
(proof existing-theorem)
(theory  pointed-ms-2-tuples))
```

```
(def-theorem non-negativity-of-distance
"forall(x,y:bfun, 0<=bfun%dist(x,y))"
(home-theory mappings-into-a-pointed-metric-space)
(translation mappings-pointed-metric-spaces-2-tuples)
(proof existing-theorem)
(usages transportable-macete)
(theory  pointed-ms-2-tuples))
```

```(def-theorem ()
"forall(x,y:bfun, bfun%dist(x,y)=bfun%dist(y,x))"
lemma
(home-theory mappings-into-a-pointed-metric-space)
(translation mappings-pointed-metric-spaces-2-tuples)
(proof existing-theorem)
(theory  pointed-ms-2-tuples))
```

```(def-theorem ()
"forall(x,y:bfun, x=y iff bfun%dist(x,y)=0)"
lemma
(home-theory mappings-into-a-pointed-metric-space)
(translation mappings-pointed-metric-spaces-2-tuples)
(proof existing-theorem)
(theory  pointed-ms-2-tuples))
```

```(def-theory-ensemble-instances
metric-spaces
(permutations (0))
(sorts (pp ms%bfun))
(constants (dist ms%bfun%dist))
(target-theories pointed-ms-2-tuples)
(special-renamings
(ball ms%bfun%ball)
(open%ball ms%bfun%open%ball)
(complete ms%bfun%complete)
(lipschitz%bound%on ms%bfun%lipschitz%bound%on)
(lipschitz%bound ms%bfun%lipschitz%bound)))
```

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

```(def-overloading dist
(pointed-ms-2-tuples ms%bfun%dist)
(metric-spaces dist))
```