let n, m be Nat; :: thesis:
A1: ( n in NAT & m in NAT & n + m in NAT ) by ORDINAL1:def 12;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
set nm = n + m;
set TRnm = TOP-REAL (n + m);
let pn be Point of (TOP-REAL n); :: thesis:
let pm be Point of (TOP-REAL m); :: thesis:
let r, s be Real; :: thesis:
assume that
A2: r > 0 and
A3: s > 0 ; :: thesis:
reconsider CLn = cl_Ball (pn,r) as non empty Subset of (TOP-REAL n) by A2;
A4: Int CLn = CLn \ (Fr CLn) by TOPS_1:40
.= CLn \ (Sphere (pn,r)) by A2, BROUWER2:5
.= CLn \ (CLn \ (Ball (pn,r))) by A1, JORDAN:19
.= CLn /\ (Ball (pn,r)) by XBOOLE_1:48
.= Ball (pn,r) by TOPREAL9:16, XBOOLE_1:28 ;
reconsider CLm = cl_Ball (pm,s) as non empty Subset of (TOP-REAL m) by A3;
A5: Int CLm = CLm \ (Fr CLm) by TOPS_1:40
.= CLm \ (Sphere (pm,s)) by A3, BROUWER2:5
.= CLm \ (CLm \ (Ball (pm,s))) by A1, JORDAN:19
.= CLm /\ (Ball (pm,s)) by XBOOLE_1:48
.= Ball (pm,s) by TOPREAL9:16, XBOOLE_1:28 ;
reconsider CLnm = cl_Ball ((0. (TOP-REAL (n + m))),1) as non empty Subset of (TOP-REAL (n + m)) ;
A6: (TOP-REAL n) | CLn = Tdisk (pn,r) by BROUWER:def 2;
A7: Ball ((0. (TOP-REAL (n + m))),1) c= CLnm by TOPREAL9:16;
A8: [#] (Tdisk ((0. (TOP-REAL (n + m))),1)) = CLnm by A1, BROUWER:3;
A9: (TOP-REAL (n + m)) | CLnm = Tdisk ((0. (TOP-REAL (n + m))),1) by BROUWER:def 2;
A10: Int CLnm = CLnm \ (Fr CLnm) by TOPS_1:40
.= CLnm \ (Sphere ((0. (TOP-REAL (n + m))),1)) by BROUWER2:5
.= CLnm \ (CLnm \ (Ball ((0. (TOP-REAL (n + m))),1))) by A1, JORDAN:19
.= CLnm /\ (Ball ((0. (TOP-REAL (n + m))),1)) by XBOOLE_1:48
.= Ball ((0. (TOP-REAL (n + m))),1) by TOPREAL9:16, XBOOLE_1:28 ;
set Rn = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1));
set Rm = ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1));
set Rnm = ClosedHypercube ((0. (TOP-REAL (n + m))),((n + m) |-> 1));
A11: [#] ((TOP-REAL m) | (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)))) = ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)) by PRE_TOPC:def 5;
A12: Ball (pn,r) c= CLn by TOPREAL9:16;
CLn is convex non boundary compact Subset of (TOP-REAL n) by A2, Lm1;
then consider fn being Function of ((TOP-REAL n) | CLn),((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) such that
A13: fn is being_homeomorphism and
A14: fn .: (Fr CLn) = Fr (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) by BROUWER2:7;
A15: fn .: (Int CLn) misses fn .: (Fr CLn) by TOPS_1:39, A13, FUNCT_1:66;
[#] ((TOP-REAL n) | (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)))) = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) by PRE_TOPC:def 5;
then A16: rng fn = ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1)) by A13, TOPS_2:def 5;
( not CLm is boundary & CLm is convex & CLm is compact ) by A3, Lm1;
then consider gm being Function of ((TOP-REAL m) | CLm),((TOP-REAL m) | (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)))) such that
A17: gm is being_homeomorphism and
A18: gm .: (Fr CLm) = Fr (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) by BROUWER2:7;
A19: (TOP-REAL m) | CLm = Tdisk (pm,s) by BROUWER:def 2;
[#] ((TOP-REAL m) | (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)))) = ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)) by PRE_TOPC:def 5;
then A20: rng gm = ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1)) by A17, TOPS_2:def 5;
A21: Ball (pm,s) c= CLm by TOPREAL9:16;
A22: [#] (Tdisk (pn,r)) = CLn by A1, BROUWER:3;
then A23: dom fn = CLn by A6, A13, TOPS_2:def 5;
( not CLnm is boundary & CLnm is convex & CLnm is compact ) by Lm1;
then consider P being Function of [:(Tdisk (pn,r)),(Tdisk (pm,s)):],(Tdisk ((0. (TOP-REAL (n + m))),1)) such that
A24: P is being_homeomorphism and
A25: for t1 being Point of ((TOP-REAL n) | CLn)
for t2 being Point of ((TOP-REAL m) | CLm) holds
( ( fn . t1 in Int (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) & gm . t2 in Int (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) ) iff P . (t1,t2) in Int CLnm ) by A6, A19, A9, Th17, A13, A17;
take P ; :: thesis:
thus P is being_homeomorphism by A24; :: thesis:
A26: gm .: (Int CLm) misses gm .: (Fr CLm) by TOPS_1:39, A17, FUNCT_1:66;
A27: [#] (Tdisk (pm,s)) = CLm by A1, BROUWER:3;
then A28: dom gm = CLm by A19, A17, TOPS_2:def 5;
A29: dom gm = CLm by A19, A17, A27, TOPS_2:def 5;
thus P .: [:(Ball (pn,r)),(Ball (pm,s)):] c= Ball ((0. (TOP-REAL (n + m))),1) :: according to XBOOLE_0:def 10 :: thesis:

proof

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A37: y in Ball ((0. (TOP-REAL (n + m))),1) ; :: thesis:
rng P = [#] (Tdisk ((0. (TOP-REAL (n + m))),1)) by TOPS_2:def 5, A24;
then consider x being object such that
A38: x in dom P and
A39: P . x = y by A37, A7, A8, FUNCT_1:def 3;
[#] [:(Tdisk (pn,r)),(Tdisk (pm,s)):] = [:([#] (Tdisk (pn,r))),([#] (Tdisk (pm,s))):] by BORSUK_1:def 2;
then consider y1, y2 being object such that
A40: y1 in CLn and
A41: y2 in CLm and
A42: x = [y1,y2] by A38, A22, A27, ZFMISC_1:def 2;
reconsider y2 = y2 as Point of ((TOP-REAL m) | CLm) by A19, A1, BROUWER:3, A41;
reconsider y1 = y1 as Point of ((TOP-REAL n) | CLn) by A6, A40, A1, BROUWER:3;
A43: P . x = P . (y1,y2) by A42;
then fn . y1 in Int (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) by A25, A39, A37, A10;
then fn . y1 in (ClosedHypercube ((0. (TOP-REAL n)),(n |-> 1))) \ (fn .: (Fr CLn)) by TOPS_1:40, A14;
then fn . y1 in (fn .: CLn) \ (fn .: (Fr CLn)) by RELAT_1:113, A23, A16;
then fn . y1 in fn .: (CLn \ (Fr CLn)) by A13, FUNCT_1:64;
then fn . y1 in fn .: (Int CLn) by TOPS_1:40;
then ex z1 being object st
( z1 in dom fn & z1 in Int CLn & fn . z1 = fn . y1 ) by FUNCT_1:def 6;
then A44: y1 in Int CLn by A23, A40, A13, FUNCT_1:def 4;
gm . y2 in Int (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) by A43, A25, A39, A37, A10;
then gm . y2 in (ClosedHypercube ((0. (TOP-REAL m)),(m |-> 1))) \ (gm .: (Fr CLm)) by TOPS_1:40, A18;
then gm . y2 in (gm .: CLm) \ (gm .: (Fr CLm)) by RELAT_1:113, A28, A20;
then gm . y2 in gm .: (CLm \ (Fr CLm)) by A17, FUNCT_1:64;
then gm . y2 in gm .: (Int CLm) by TOPS_1:40;
then ex z2 being object st
( z2 in dom gm & z2 in Int CLm & gm . z2 = gm . y2 ) by FUNCT_1:def 6;
then y2 in Int CLm by A28, A41, A17, FUNCT_1:def 4;
then [y1,y2] in [:(Ball (pn,r)),(Ball (pm,s)):] by A44, A5, A4, ZFMISC_1:87;
hence y in P .: [:(Ball (pn,r)),(Ball (pm,s)):] by A38, A39, A42, FUNCT_1:def 6; :: thesis: