let n, m be Nat; :: thesis:
let T1, T2 be non empty TopSpace; :: thesis:
let pn be Point of (TOP-REAL n); :: thesis:
let pm be Point of (TOP-REAL m); :: thesis:
set nm = n + m;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
set TRnm = TOP-REAL (n + m);
let r, s be Real; :: thesis:
assume that
A1: r > 0 and
A2: s > 0 ; :: thesis:
set Rn = n |-> r;
set Rm = m |-> s;
set Rnm = (n + m) |-> 1;
set RR = ClosedHypercube (pn,(n |-> r));
set RS = ClosedHypercube (pm,(m |-> s));
set CL = ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1));
reconsider Rs = ClosedHypercube (pm,(m |-> s)) as non empty Subset of (TOP-REAL m) by A2;
reconsider Rr = ClosedHypercube (pn,(n |-> r)) as non empty Subset of (TOP-REAL n) by A1;
set Or = OpenHypercube (pn,r);
set Os = OpenHypercube (pm,s);
set O = OpenHypercube ((0. (TOP-REAL (n + m))),1);
consider h being Function of [:((TOP-REAL n) | Rr),((TOP-REAL m) | Rs):],((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) such that
A3: h is being_homeomorphism and
A4: h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] = OpenHypercube ((0. (TOP-REAL (n + m))),1) by Th15, A1, A2;
let f be Function of T1,((TOP-REAL n) | (ClosedHypercube (pn,(n |-> r)))); :: thesis:
let g be Function of T2,((TOP-REAL m) | (ClosedHypercube (pm,(m |-> s)))); :: thesis:
assume that
A5: f is being_homeomorphism and
A6: g is being_homeomorphism ; :: thesis:
A7: dom g = [#] T2 by A6, TOPS_2:def 5;
reconsider G = g as Function of T2,((TOP-REAL m) | Rs) ;
reconsider F = f as Function of T1,((TOP-REAL n) | Rr) ;
reconsider fgh = h * [:F,G:] as Function of [:T1,T2:],((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) ;
take fgh ; :: thesis:
[:F,G:] is being_homeomorphism by A5, A6, Th14;
hence fgh is being_homeomorphism by A3, TOPS_2:57; :: thesis:
then A8: dom fgh = [#] [:T1,T2:] by TOPS_2:def 5;
let t1 be Point of T1; :: thesis:
let t2 be Point of T2; :: thesis:
dom f = [#] T1 by A5, TOPS_2:def 5;
then A9: [(f . t1),(g . t2)] = [:F,G:] . (t1,t2) by A7, FUNCT_3:def 8
.= [:F,G:] . [t1,t2] ;
A10: [#] ((TOP-REAL m) | Rs) = Rs by PRE_TOPC:def 5;
[#] ((TOP-REAL n) | Rr) = Rr by PRE_TOPC:def 5;
then A11: [#] [:((TOP-REAL n) | Rr),((TOP-REAL m) | Rs):] = [:Rr,Rs:] by A10, BORSUK_1:def 2;
A12: OpenHypercube (pm,s) c= Rs by Th12;
A13: OpenHypercube (pn,r) c= Rr by Th12;
A14: dom h = [#] [:((TOP-REAL n) | Rr),((TOP-REAL m) | Rs):] by A3, TOPS_2:def 5;
thus ( f . t1 in OpenHypercube (pn,r) & g . t2 in OpenHypercube (pm,s) implies fgh . (t1,t2) in OpenHypercube ((0. (TOP-REAL (n + m))),1) ) :: thesis:

proof

assume that
A15: f . t1 in OpenHypercube (pn,r) and
A16: g . t2 in OpenHypercube (pm,s) ; :: thesis:
A17: [(f . t1),(g . t2)] in [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] by ZFMISC_1:87, A15, A16;
[(f . t1),(g . t2)] in dom h by A15, A13, A16, A12, A11, A14, ZFMISC_1:87;
then h . [(f . t1),(g . t2)] in OpenHypercube ((0. (TOP-REAL (n + m))),1) by A17, A4, FUNCT_1:def 6;
hence fgh . (t1,t2) in OpenHypercube ((0. (TOP-REAL (n + m))),1) by A8, A9, FUNCT_1:12; :: thesis:

end;

assume A18: fgh . (t1,t2) in OpenHypercube ((0. (TOP-REAL (n + m))),1) ; :: thesis:
fgh . (t1,t2) = h . [(f . t1),(g . t2)] by A8, FUNCT_1:12, A9;
then consider xy being object such that
A19: xy in dom h and
A20: xy in [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] and
A21: h . xy = h . [(f . t1),(g . t2)] by A18, FUNCT_1:def 6, A4;
[(f . t1),(g . t2)] in dom h by A8, FUNCT_1:11, A9;
then xy = [(f . t1),(g . t2)] by A19, A21, A3, FUNCT_1:def 4;
hence ( f . t1 in OpenHypercube (pn,r) & g . t2 in OpenHypercube (pm,s) ) by A20, ZFMISC_1:87; :: thesis: