let n, m be Nat; :: thesis: 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) )
let pn be Point of (TOP-REAL n); :: thesis: 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) )
let pm be Point of (TOP-REAL m); :: thesis: 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) )
let r, s be Real; :: thesis: ( r > 0 & s > 0 implies 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) ) )
assume that
A1: r > 0 and
A2: s > 0 ; :: thesis: 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) )
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
set nm = n + m;
set TRnm = TOP-REAL (n + m);
set RN = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1));
set RR = ClosedHypercube (pn,(n |-> r));
set RS = ClosedHypercube (pm,(m |-> s));
set RM = ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1));
set RNM = ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1));
reconsider Rs = ClosedHypercube (pm,(m |-> s)), Rm = ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)) as non empty Subset of (TOP-REAL m) by A2;
consider hm being Function of ((TOP-REAL m) | Rs),((TOP-REAL m) | Rm) such that
A3: hm is being_homeomorphism and
A4: hm .: (Fr Rs) = Fr Rm by A2, BROUWER2:7;
A5: dom hm = [#] ((TOP-REAL m) | Rs) by A3, TOPS_2:def 5;
0. (TOP-REAL m) = 0* m by EUCLID:70;
then A6: 0. (TOP-REAL m) = m |-> 0 by EUCLID:def 4;
0. (TOP-REAL n) = 0* n by EUCLID:70;
then A7: 0. (TOP-REAL n) = n |-> 0 by EUCLID:def 4;
reconsider Rr = ClosedHypercube (pn,(n |-> r)), Rn = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) as non empty Subset of (TOP-REAL n) by A1;
consider hn being Function of ((TOP-REAL n) | Rr),((TOP-REAL n) | Rn) such that
A8: hn is being_homeomorphism and
A9: hn .: (Fr Rr) = Fr Rn by A1, BROUWER2:7;
A10: dom hn = [#] ((TOP-REAL n) | Rr) by A8, TOPS_2:def 5;
set Or = OpenHypercube (pn,r);
set Os = OpenHypercube (pm,s);
set OO = OpenHypercube ((0. (TOP-REAL (n + m))),1);
A11: [#] ((TOP-REAL (n + m)) | (ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)))) = ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)) by PRE_TOPC:def 5;
A12: Int Rs = OpenHypercube (pm,s) by A2, Th11;
then A13: hm .: (OpenHypercube (pm,s)) misses hm .: (Fr Rs) by TOPS_1:39, FUNCT_1:66, A3;
A14: [#] ((TOP-REAL m) | Rm) = Rm by PRE_TOPC:def 5;
0. (TOP-REAL (n + m)) = 0* (n + m) by EUCLID:70;
then A15: 0. (TOP-REAL (n + m)) = (n + m) |-> 0 by EUCLID:def 4;
set ON = OpenHypercube ((0. (TOP-REAL n)),1);
set Om = OpenHypercube ((0. (TOP-REAL m)),1);
reconsider Rnm = ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1)) as non empty Subset of (TOP-REAL (n + m)) ;
A16: n in NAT by ORDINAL1:def 12;
m in NAT by ORDINAL1:def 12;
then consider f being Function of [:(TOP-REAL n),(TOP-REAL m):],(TOP-REAL (n + m)) such that
A17: f is being_homeomorphism and
A18: for fi being Element of (TOP-REAL n)
for fj being Element of (TOP-REAL m) holds f . (fi,fj) = fi ^ fj by A16, SIMPLEX2:19;
A19: [#] ((TOP-REAL m) | Rs) = Rs by PRE_TOPC:def 5;
A20: the carrier of [:(TOP-REAL n),(TOP-REAL m):] = [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL m):] by BORSUK_1:def 2;
A21: f .: [:Rn,Rm:] c= Rnm
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: [:Rn,Rm:] or y in Rnm )
assume A22: y in f .: [:Rn,Rm:] ; :: thesis: y in Rnm
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: ( i in Seg (n + m) implies pq . i in [.(((0. (TOP-REAL (n + m))) . i) - (((n + m) |-> 1) . i)),(((0. (TOP-REAL (n + m))) . i) + (((n + m) |-> 1) . i)).] )
assume A35: i in Seg (n + m) ; :: thesis: pq . i in [.(((0. (TOP-REAL (n + m))) . i) - (((n + m) |-> 1) . i)),(((0. (TOP-REAL (n + m))) . i) + (((n + m) |-> 1) . i)).]
A36: ((n + m) |-> 1) . i = 1 by A35, FINSEQ_2:57;
A37: (0. (TOP-REAL (n + m))) . i = 0 by A15;
per cases ( i in dom p or ex k being Nat st
( k in dom q & i = (len p) + k ) ) by A34, A35, FINSEQ_1:25;
suppose A38: i in dom p ; :: thesis: pq . i in [.(((0. (TOP-REAL (n + m))) . i) - (((n + m) |-> 1) . i)),(((0. (TOP-REAL (n + m))) . i) + (((n + m) |-> 1) . i)).]
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: verum
end;
suppose ex k being Nat st
( k in dom q & i = (len p) + k ) ; :: thesis: pq . i in [.(((0. (TOP-REAL (n + m))) . i) - (((n + m) |-> 1) . i)),(((0. (TOP-REAL (n + m))) . i) + (((n + m) |-> 1) . i)).]
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: verum
end;
end;
end;
hence y in Rnm by Def2, A30, A25; :: thesis: verum
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: ( not x in Rnm or x in f .: [:Rn,Rm:] )
assume A46: x in Rnm ; :: thesis: x in f .: [:Rn,Rm:]
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: for i being Nat st i in Seg n holds
p . i in [.(((0. (TOP-REAL n)) . i) - ((n |-> 1) . i)),(((0. (TOP-REAL n)) . i) + ((n |-> 1) . i)).]
let i be Nat; :: thesis: ( i in Seg n implies p . i in [.(((0. (TOP-REAL n)) . i) - ((n |-> 1) . i)),(((0. (TOP-REAL n)) . i) + ((n |-> 1) . i)).] )
assume A52: i in Seg n ; :: thesis: p . i in [.(((0. (TOP-REAL n)) . i) - ((n |-> 1) . i)),(((0. (TOP-REAL n)) . i) + ((n |-> 1) . i)).]
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: verum
end;
then A57: p in Rn by Def2;
A58: dom q = Seg m by A48, FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in Seg m holds
q . i in [.(((0. (TOP-REAL m)) . i) - ((m |-> 1) . i)),(((0. (TOP-REAL m)) . i) + ((m |-> 1) . i)).]
let i be Nat; :: thesis: ( i in Seg m implies q . i in [.(((0. (TOP-REAL m)) . i) - ((m |-> 1) . i)),(((0. (TOP-REAL m)) . i) + ((m |-> 1) . i)).] )
assume A59: i in Seg m ; :: thesis: q . i in [.(((0. (TOP-REAL m)) . i) - ((m |-> 1) . i)),(((0. (TOP-REAL m)) . i) + ((m |-> 1) . i)).]
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: verum
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: verum
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: ( h is being_homeomorphism & h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] = OpenHypercube ((0. (TOP-REAL (n + m))),1) )
A72: f1 is being_homeomorphism by A17, A71, METRIZTS:2, A64;
hence h is being_homeomorphism by A67, TOPS_2:57; :: thesis: h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] = OpenHypercube ((0. (TOP-REAL (n + m))),1)
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: OpenHypercube ((0. (TOP-REAL (n + m))),1) c= h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):]
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] or y in OpenHypercube ((0. (TOP-REAL (n + m))),1) )
assume A79: y in h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] ; :: thesis: y in OpenHypercube ((0. (TOP-REAL (n + m))),1)
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: ( i in Seg (n + m) implies hpq . i in ].(((0. (TOP-REAL (n + m))) . i) - 1),(((0. (TOP-REAL (n + m))) . i) + 1).[ )
assume A98: i in Seg (n + m) ; :: thesis: hpq . i in ].(((0. (TOP-REAL (n + m))) . i) - 1),(((0. (TOP-REAL (n + m))) . i) + 1).[
A99: (0. (TOP-REAL (n + m))) . i = 0 by A15;
per cases ( i in dom hnp or ex k being Nat st
( k in dom hmq & i = (len hnp) + k ) ) by A97, A98, FINSEQ_1:25;
suppose A100: i in dom hnp ; :: thesis: hpq . i in ].(((0. (TOP-REAL (n + m))) . i) - 1),(((0. (TOP-REAL (n + m))) . i) + 1).[
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: verum
end;
suppose ex k being Nat st
( k in dom hmq & i = (len hnp) + k ) ; :: thesis: hpq . i in ].(((0. (TOP-REAL (n + m))) . i) - 1),(((0. (TOP-REAL (n + m))) . i) + 1).[
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: verum
end;
end;
end;
hence y in OpenHypercube ((0. (TOP-REAL (n + m))),1) by Th3, A93, A92; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in OpenHypercube ((0. (TOP-REAL (n + m))),1) or y in h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):] )
assume A105: y in OpenHypercube ((0. (TOP-REAL (n + m))),1) ; :: thesis: y in h .: [:(OpenHypercube (pn,r)),(OpenHypercube (pm,s)):]
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: for i being Nat st i in Seg m holds
q . i in ].(((0. (TOP-REAL m)) . i) - 1),(((0. (TOP-REAL m)) . i) + 1).[
let i be Nat; :: thesis: ( i in Seg m implies q . i in ].(((0. (TOP-REAL m)) . i) - 1),(((0. (TOP-REAL m)) . i) + 1).[ )
assume A111: i in Seg m ; :: thesis: q . i in ].(((0. (TOP-REAL m)) . i) - 1),(((0. (TOP-REAL m)) . i) + 1).[
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: verum
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: for i being Nat st i in Seg n holds
p . i in ].(((0. (TOP-REAL n)) . i) - 1),(((0. (TOP-REAL n)) . i) + 1).[
A119: Seg n c= Seg (n + m) by NAT_1:11, FINSEQ_1:5;
let i be Nat; :: thesis: ( i in Seg n implies p . i in ].(((0. (TOP-REAL n)) . i) - 1),(((0. (TOP-REAL n)) . i) + 1).[ )
assume A120: i in Seg n ; :: thesis: p . i in ].(((0. (TOP-REAL n)) . i) - 1),(((0. (TOP-REAL n)) . i) + 1).[
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: verum
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: verum