theorem Th18:
for
n,
m being
Nat for
pn being
Point of
(TOP-REAL n) for
pm being
Point of
(TOP-REAL m) for
r,
s being
Real st
r > 0 &
s > 0 holds
ex
h being
Function of
[:(Tdisk (pn,r)),(Tdisk (pm,s)):],
(Tdisk ((0. (TOP-REAL (n + m))),1)) st
(
h is
being_homeomorphism &
h .: [:(Ball (pn,r)),(Ball (pm,s)):] = Ball (
(0. (TOP-REAL (n + m))),1) )