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