theorem Th15: :: TIETZE_2:16

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 [:((TOP-REAL n) | (ClosedHypercube (pn,(n |-> r)))),((TOP-REAL m) | (ClosedHypercube (pm,(m |-> s)))):],((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) st
( h is being_homeomorphism & h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] = OpenHypercube ((0. (TOP-REAL (n + m))),1) )