theorem Th16:
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) ) ) )