for n, m being Nat
for T1, T2 being non empty TopSpace
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
for f being Function of T1,((TOP-REAL n) | (ClosedHypercube (pn,(n |-> r))))
for g being Function of T2,((TOP-REAL m) | (ClosedHypercube (pm,(m |-> s)))) st f is being_homeomorphism & g is being_homeomorphism holds
ex h being Function of [:T1,T2:],((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) st
( h is being_homeomorphism & ( for t1 being Point of T1
for t2 being Point of T2 holds
( ( f . t1 in OpenHypercube (pn,r) & g . t2 in OpenHypercube (pm,s) ) iff h . (t1,t2) in OpenHypercube ((0. (TOP-REAL (n + m))),1) ) ) )