for n, m being Nat
for r, s being Real
for T1, T2 being non empty TopSpace
for pn being Point of (TOP-REAL n)
for pm being Point of (TOP-REAL m) st r > 0 & s > 0 & T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic & T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic holds
[:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic