proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A22: y in f .: [:Rn,Rm:] ; :: thesis:
then consider x being object such that
A23: x in dom f and
A24: x in [:Rn,Rm:] and
A25: f . x = y by FUNCT_1:def 6;
consider p, q being object such that
A26: p in the carrier of (TOP-REAL n) and
A27: q in the carrier of (TOP-REAL m) and
A28: x = [p,q] by A20, A23, ZFMISC_1:def 2;
reconsider q = q as Point of (TOP-REAL m) by A27;
A29: q in Rm by A24, A28, ZFMISC_1:87;
reconsider p = p as Point of (TOP-REAL n) by A26;
A30: f . x = f . (p,q) by A28
.= p ^ q by A18 ;
then reconsider pq = p ^ q as Point of (TOP-REAL (n + m)) by A25, A22;
A31: p in Rn by A24, A28, ZFMISC_1:87;
for i being Nat st i in Seg (n + m) holds
pq . i in [.(((0. (TOP-REAL (n + m))) . i) - (((n + m) |-> 1) . i)),(((0. (TOP-REAL (n + m))) . i) + (((n + m) |-> 1) . i)).]

proof

len q = m by CARD_1:def 7;
then A32: dom q = Seg m by FINSEQ_1:def 3;
len p = n by CARD_1:def 7;
then A33: dom p = Seg n by FINSEQ_1:def 3;
len pq = n + m by CARD_1:def 7;
then A34: dom pq = Seg (n + m) by FINSEQ_1:def 3;
let i be Nat; :: thesis:
assume A35: i in Seg (n + m) ; :: thesis:
A36: ((n + m) |-> 1) . i = 1 by A35, FINSEQ_2:57;
A37: (0. (TOP-REAL (n + m))) . i = 0 by A15;

per cases by A34, A35, FINSEQ_1:25;

suppose A38: i in dom p ; :: thesis:

then A39: pq . i = p . i by FINSEQ_1:def 7;
A40: (0. (TOP-REAL n)) . i = 0 by A7;
(n |-> 1) . i = 1 by A38, A33, FINSEQ_2:57;
hence pq . i in [.(((0. (TOP-REAL (n + m))) . i) - (((n + m) |-> 1) . i)),(((0. (TOP-REAL (n + m))) . i) + (((n + m) |-> 1) . i)).] by A40, A39, A38, Def2, A33, A31, A37, A36; :: thesis:

end;

suppose ex k being Nat st
( k in dom q & i = (len p) + k ) ; :: thesis:

then consider k being Nat such that
A41: k in dom q and
A42: i = (len p) + k ;
A43: (m |-> 1) . k = 1 by A41, A32, FINSEQ_2:57;
A44: (0. (TOP-REAL m)) . k = 0 by A6;
pq . i = q . k by FINSEQ_1:def 7, A41, A42;
hence pq . i in [.(((0. (TOP-REAL (n + m))) . i) - (((n + m) |-> 1) . i)),(((0. (TOP-REAL (n + m))) . i) + (((n + m) |-> 1) . i)).] by A44, A43, Def2, A32, A29, A41, A37, A36; :: thesis:

end;

hence y in Rnm by Def2, A30, A25; :: thesis:

end;

A45: dom f = [#] [:(TOP-REAL n),(TOP-REAL m):] by A17, TOPS_2:def 5;
Rnm c= f .: [:Rn,Rm:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A46: x in Rnm ; :: thesis:
then reconsider pq = x as Point of (TOP-REAL (n + m)) ;
rng pq c= REAL ;
then reconsider pq = pq as FinSequence of REAL by FINSEQ_1:def 4;
len pq = n + m by CARD_1:def 7;
then consider p, q being FinSequence of REAL such that
A47: len p = n and
A48: len q = m and
A49: pq = p ^ q by FINSEQ_2:23;
reconsider p = p as Point of (TOP-REAL n) by TOPREAL7:17, A47;
reconsider q = q as Point of (TOP-REAL m) by TOPREAL7:17, A48;
A50: f . [p,q] = f . (p,q)
.= p ^ q by A18 ;
A51: dom p = Seg n by A47, FINSEQ_1:def 3;

now :: thesis:

let i be Nat; :: thesis:
assume A52: i in Seg n ; :: thesis:
A53: (0. (TOP-REAL (n + m))) . i = 0 by A15;
A54: Seg n c= Seg (n + m) by NAT_1:11, FINSEQ_1:5;
then ((n + m) |-> 1) . i = 1 by A52, FINSEQ_2:57;
then A55: pq . i in [.(0 - 1),(0 + 1).] by A53, A54, A52, A46, Def2;
A56: (0. (TOP-REAL n)) . i = 0 by A7;
(n |-> 1) . i = 1 by A52, FINSEQ_2:57;
hence p . i in [.(((0. (TOP-REAL n)) . i) - ((n |-> 1) . i)),(((0. (TOP-REAL n)) . i) + ((n |-> 1) . i)).] by A49, FINSEQ_1:def 7, A51, A52, A56, A55; :: thesis:

end;

then A57: p in Rn by Def2;
A58: dom q = Seg m by A48, FINSEQ_1:def 3;

now :: thesis:

let i be Nat; :: thesis:
assume A59: i in Seg m ; :: thesis:
A60: (m |-> 1) . i = 1 by A59, FINSEQ_2:57;
A61: ((n + m) |-> 1) . (i + n) = 1 by A59, FINSEQ_1:60, FINSEQ_2:57;
A62: (0. (TOP-REAL m)) . i = 0 by A6;
A63: (0. (TOP-REAL (n + m))) . (i + n) = 0 by A15;
i + n in Seg (n + m) by A59, FINSEQ_1:60;
then pq . (i + n) in [.(0 - 1),(0 + 1).] by A61, A63, A46, Def2;
hence q . i in [.(((0. (TOP-REAL m)) . i) - ((m |-> 1) . i)),(((0. (TOP-REAL m)) . i) + ((m |-> 1) . i)).] by A47, A49, FINSEQ_1:def 7, A58, A59, A60, A62; :: thesis:

end;

then q in Rm by Def2;
then [p,q] in [:Rn,Rm:] by A57, ZFMISC_1:87;
hence x in f .: [:Rn,Rm:] by A50, A49, A45, FUNCT_1:def 6; :: thesis:

end;

then A64: Rnm = f .: [:Rn,Rm:] by A21;
A65: [#] ((TOP-REAL n) | Rr) = Rr by PRE_TOPC:def 5;
then A66: the carrier of [:((TOP-REAL n) | Rr),((TOP-REAL m) | Rs):] = [:Rr,Rs:] by BORSUK_1:def 2, A19;
set hnm = [:hn,hm:];
A67: [:hn,hm:] is being_homeomorphism by A8, A3, Th14;
then A68: dom [:hn,hm:] = [#] [:((TOP-REAL n) | Rr),((TOP-REAL m) | Rs):] by TOPS_2:def 5;
A69: Int Rn = OpenHypercube ((0. (TOP-REAL n)),1) by Th11;
then A70: OpenHypercube ((0. (TOP-REAL n)),1) c= Rn by TOPS_1:16;
A71: [:(TOP-REAL n),(TOP-REAL m):] | [:Rn,Rm:] = [:((TOP-REAL n) | Rn),((TOP-REAL m) | Rm):] by BORSUK_3:22;
then reconsider f1 = f | [:Rn,Rm:] as Function of [:((TOP-REAL n) | Rn),((TOP-REAL m) | Rm):],((TOP-REAL (n + m)) | Rnm) by A64, JORDAN24:12;
reconsider h = f1 * [:hn,hm:] as 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)))) ;
take h ; :: thesis:
A72: f1 is being_homeomorphism by A17, A71, METRIZTS:2, A64;
hence h is being_homeomorphism by A67, TOPS_2:57; :: thesis:
A73: [#] ((TOP-REAL n) | Rn) = Rn by PRE_TOPC:def 5;
dom f1 = [#] [:((TOP-REAL n) | Rn),((TOP-REAL m) | Rm):] by A72, TOPS_2:def 5;
then A74: dom f1 = [:Rn,Rm:] by BORSUK_1:def 2, A73, A14;
A75: Int Rm = OpenHypercube ((0. (TOP-REAL m)),1) by Th11;
then A76: OpenHypercube ((0. (TOP-REAL m)),1) c= Rm by TOPS_1:16;
A77: Int Rr = OpenHypercube (pn,r) by A1, Th11;
then A78: hn .: (OpenHypercube (pn,r)) misses hn .: (Fr Rr) by TOPS_1:39, FUNCT_1:66, A8;
thus h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] c= OpenHypercube ((0. (TOP-REAL (n + m))),1) :: according to XBOOLE_0:def 10 :: thesis:

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A79: y in h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] ; :: thesis:
then consider x being object such that
A80: x in dom h and
A81: x in [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] and
A82: h . x = y by FUNCT_1:def 6;
consider p, q being object such that
A83: p in Rr and
A84: q in Rs and
A85: [p,q] = x by A80, A66, ZFMISC_1:def 2;
reconsider p = p as Point of (TOP-REAL n) by A83;
A86: hn . p in rng hn by A83, A10, A65, FUNCT_1:def 3;
reconsider q = q as Point of (TOP-REAL m) by A84;
A87: hm . q in rng hm by A84, A5, A19, FUNCT_1:def 3;
p in OpenHypercube (pn,r) by A81, A85, ZFMISC_1:87;
then hn . p in hn .: (OpenHypercube (pn,r)) by A83, A10, A65, FUNCT_1:def 6;
then not hn . p in Fr Rn by XBOOLE_0:3, A78, A9;
then A88: hn . p in Rn \ (Fr Rn) by A86, A73, XBOOLE_0:def 5;
then reconsider hnp = hn . p as Point of (TOP-REAL n) ;
A89: h . x = f1 . ([:hn,hm:] . x) by A80, FUNCT_1:12;
q in OpenHypercube (pm,s) by A81, A85, ZFMISC_1:87;
then hm . q in hm .: (OpenHypercube (pm,s)) by A84, A5, A19, FUNCT_1:def 6;
then not hm . q in Fr Rm by XBOOLE_0:3, A13, A4;
then A90: hm . q in Rm \ (Fr Rm) by A87, A14, XBOOLE_0:def 5;
then reconsider hmq = hm . q as Point of (TOP-REAL m) ;
A91: hm . q in OpenHypercube ((0. (TOP-REAL m)),1) by A90, TOPS_1:40, A75;
[:hn,hm:] . x = [:hn,hm:] . (p,q) by A85;
then A92: y = f1 . [hnp,hmq] by A82, A89, A83, A84, A10, A65, A5, A19, FUNCT_3:def 8;
A93: f1 . [hnp,hmq] = f . (hnp,hmq) by A86, A87, A73, A14, ZFMISC_1:87, FUNCT_1:49
.= hnp ^ hmq by A18 ;
then hnp ^ hmq in [#] ((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) by A92, A79;
then reconsider hpq = hnp ^ hmq as Point of (TOP-REAL (n + m)) by A11;
A94: hn . p in OpenHypercube ((0. (TOP-REAL n)),1) by A88, TOPS_1:40, A69;
for i being Nat st i in Seg (n + m) holds
hpq . i in ].(((0. (TOP-REAL (n + m))) . i) - 1),(((0. (TOP-REAL (n + m))) . i) + 1).[

proof

len hmq = m by CARD_1:def 7;
then A95: dom hmq = Seg m by FINSEQ_1:def 3;
len hnp = n by CARD_1:def 7;
then A96: dom hnp = Seg n by FINSEQ_1:def 3;
len hpq = n + m by CARD_1:def 7;
then A97: dom hpq = Seg (n + m) by FINSEQ_1:def 3;
let i be Nat; :: thesis:
assume A98: i in Seg (n + m) ; :: thesis:
A99: (0. (TOP-REAL (n + m))) . i = 0 by A15;

per cases by A97, A98, FINSEQ_1:25;

suppose A100: i in dom hnp ; :: thesis:

A101: (0. (TOP-REAL n)) . i = 0 by A7;
hnp . i in ].(((0. (TOP-REAL n)) . i) - 1),(((0. (TOP-REAL n)) . i) + 1).[ by A100, A94, A96, Th3;
hence hpq . i in ].(((0. (TOP-REAL (n + m))) . i) - 1),(((0. (TOP-REAL (n + m))) . i) + 1).[ by A101, A100, FINSEQ_1:def 7, A99; :: thesis:

end;

suppose ex k being Nat st
( k in dom hmq & i = (len hnp) + k ) ; :: thesis:

then consider k being Nat such that
A102: k in dom hmq and
A103: i = (len hnp) + k ;
A104: (0. (TOP-REAL m)) . k = 0 by A6;
hmq . k in ].(((0. (TOP-REAL m)) . k) - 1),(((0. (TOP-REAL m)) . k) + 1).[ by A95, A102, Th3, A91;
hence hpq . i in ].(((0. (TOP-REAL (n + m))) . i) - 1),(((0. (TOP-REAL (n + m))) . i) + 1).[ by A104, FINSEQ_1:def 7, A102, A103, A99; :: thesis:

end;

hence y in OpenHypercube ((0. (TOP-REAL (n + m))),1) by Th3, A93, A92; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A105: y in OpenHypercube ((0. (TOP-REAL (n + m))),1) ; :: thesis:
then reconsider pq = y as Point of (TOP-REAL (n + m)) ;
rng pq c= REAL ;
then reconsider pq = pq as FinSequence of REAL by FINSEQ_1:def 4;
len pq = n + m by CARD_1:def 7;
then consider p, q being FinSequence of REAL such that
A106: len p = n and
A107: len q = m and
A108: pq = p ^ q by FINSEQ_2:23;
reconsider q = q as Point of (TOP-REAL m) by TOPREAL7:17, A107;
A109: dom q = Seg m by A107, FINSEQ_1:def 3;

A110: now :: thesis:

let i be Nat; :: thesis:
assume A111: i in Seg m ; :: thesis:
A112: (0. (TOP-REAL (n + m))) . (i + n) = 0 by A15;
A113: (0. (TOP-REAL m)) . i = 0 by A6;
i + n in Seg (n + m) by A111, FINSEQ_1:60;
then pq . (i + n) in ].(0 - 1),(0 + 1).[ by A112, A105, Th3;
hence q . i in ].(((0. (TOP-REAL m)) . i) - 1),(((0. (TOP-REAL m)) . i) + 1).[ by A106, A108, FINSEQ_1:def 7, A109, A111, A113; :: thesis:

end;

then A114: q in OpenHypercube ((0. (TOP-REAL m)),1) by Th3;
q in Rm by A76, Th3, A110;
then q in rng hm by A3, TOPS_2:def 5, A14;
then consider xq being object such that
A115: xq in dom hm and
A116: hm . xq = q by FUNCT_1:def 3;
reconsider p = p as Point of (TOP-REAL n) by TOPREAL7:17, A106;
A117: dom p = Seg n by A106, FINSEQ_1:def 3;

A118: now :: thesis:

A119: Seg n c= Seg (n + m) by NAT_1:11, FINSEQ_1:5;
let i be Nat; :: thesis:
assume A120: i in Seg n ; :: thesis:
A121: (0. (TOP-REAL n)) . i = 0 by A7;
(0. (TOP-REAL (n + m))) . i = 0 by A15;
then pq . i in ].(0 - 1),(0 + 1).[ by A119, A120, A105, Th3;
hence p . i in ].(((0. (TOP-REAL n)) . i) - 1),(((0. (TOP-REAL n)) . i) + 1).[ by A108, FINSEQ_1:def 7, A117, A120, A121; :: thesis:

end;

then A122: p in OpenHypercube ((0. (TOP-REAL n)),1) by Th3;
p in Rn by Th3, A118, A70;
then p in rng hn by A8, TOPS_2:def 5, A73;
then consider xp being object such that
A123: xp in dom hn and
A124: hn . xp = p by FUNCT_1:def 3;
reconsider xq = xq as Point of (TOP-REAL m) by A115, A5, A19;
reconsider xp = xp as Point of (TOP-REAL n) by A123, A10, A65;
A125: [xp,xq] in [:Rr,Rs:] by A65, A123, A115, A19, ZFMISC_1:87;
A126: [p,q] = [:hn,hm:] . (xp,xq) by FUNCT_3:def 8, A115, A116, A123, A124
.= [:hn,hm:] . [xp,xq] ;
[p,q] in [:Rn,Rm:] by A70, A122, A76, A114, ZFMISC_1:87;
then A127: [xp,xq] in dom h by A125, A68, A66, A126, A74, FUNCT_1:11;
not q in Fr Rm by A114, A75, TOPS_1:39, XBOOLE_0:3;
then not xq in Fr Rs by A4, A115, A116, FUNCT_1:def 6;
then xq in Rs \ (Fr Rs) by A115, A19, XBOOLE_0:def 5;
then A128: xq in OpenHypercube (pm,s) by A12, TOPS_1:40;
not p in Fr Rn by A122, A69, TOPS_1:39, XBOOLE_0:3;
then not xp in Fr Rr by A9, A123, A124, FUNCT_1:def 6;
then xp in Rr \ (Fr Rr) by A123, A65, XBOOLE_0:def 5;
then xp in OpenHypercube (pn,r) by A77, TOPS_1:40;
then A129: [xp,xq] in [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] by A128, ZFMISC_1:87;
f1 . [p,q] = f . (p,q) by A70, A122, A76, A114, ZFMISC_1:87, FUNCT_1:49
.= p ^ q by A18 ;
then h . [xp,xq] = y by A127, A126, FUNCT_1:12, A108;
hence y in h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] by A129, A127, FUNCT_1:def 6; :: thesis: