let n, m be Nat; :: thesis: for r, s being Real
for T1, T2 being non empty TopSpace
for pn being Point of (TOP-REAL n)
for pm being Point of (TOP-REAL m) st r > 0 & s > 0 & T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic & T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic holds
[:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic
let r, s be Real; :: thesis: for T1, T2 being non empty TopSpace
for pn being Point of (TOP-REAL n)
for pm being Point of (TOP-REAL m) st r > 0 & s > 0 & T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic & T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic holds
[:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic
let T1, T2 be non empty TopSpace; :: thesis: for pn being Point of (TOP-REAL n)
for pm being Point of (TOP-REAL m) st r > 0 & s > 0 & T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic & T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic holds
[:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic
let pn be Point of (TOP-REAL n); :: thesis: for pm being Point of (TOP-REAL m) st r > 0 & s > 0 & T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic & T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic holds
[:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic
let pm be Point of (TOP-REAL m); :: thesis: ( r > 0 & s > 0 & T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic & T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic implies [:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic )
reconsider N = n, M = m as Element of 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);
reconsider Pn = pn as Point of (TOP-REAL N) ;
reconsider Pm = pm as Point of (TOP-REAL M) ;
assume that
A1: r > 0 and
A2: s > 0 ; :: thesis: ( not T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic or not T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic or [:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic )
reconsider Bm = Ball (Pm,s) as non empty Subset of (TOP-REAL M) by A2;
A3: [#] (Tdisk (Pm,s)) = cl_Ball (Pm,s) by BROUWER:3;
then reconsider BBm = Ball (Pm,s) as Subset of (Tdisk (Pm,s)) by TOPREAL9:16;
A4: Tdisk (Pm,s) = (TOP-REAL M) | (cl_Ball (Pm,s)) by BROUWER:def 2;
then A5: (Tdisk (Pm,s)) | BBm = (TOP-REAL M) | (Ball (Pm,s)) by A3, PRE_TOPC:7;
reconsider Bn = Ball (Pn,r) as non empty Subset of (TOP-REAL N) by A1;
reconsider Bnm = Ball ((0. (TOP-REAL (N + M))),1) as non empty Subset of (TOP-REAL (N + M)) ;
A6: [#] (Tdisk (Pn,r)) = cl_Ball (pn,r) by BROUWER:3;
then reconsider BBn = Ball (Pn,r) as Subset of (Tdisk (Pn,r)) by TOPREAL9:16;
A7: [#] (Tdisk ((0. (TOP-REAL (N + M))),1)) = cl_Ball ((0. (TOP-REAL (N + M))),1) by BROUWER:3;
then reconsider BBnm = Ball ((0. (TOP-REAL (N + M))),1) as Subset of (Tdisk ((0. (TOP-REAL (N + M))),1)) by TOPREAL9:16;
A8: Tdisk ((0. (TOP-REAL (N + M))),1) = (TOP-REAL (N + M)) | (cl_Ball ((0. (TOP-REAL (N + M))),1)) by BROUWER:def 2;
then A9: (Tdisk ((0. (TOP-REAL (N + M))),1)) | BBnm = (TOP-REAL (N + M)) | (Ball ((0. (TOP-REAL (N + M))),1)) by A7, PRE_TOPC:7;
assume T1,(TOP-REAL n) | (Ball (pn,r)) are_homeomorphic ; :: thesis: ( not T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic or [:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic )
then consider f1 being Function of T1,((TOP-REAL N) | Bn) such that
A10: f1 is being_homeomorphism by T_0TOPSP:def 1;
assume T2,(TOP-REAL m) | (Ball (pm,s)) are_homeomorphic ; :: thesis: [:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic
then consider f2 being Function of T2,((TOP-REAL M) | Bm) such that
A11: f2 is being_homeomorphism by T_0TOPSP:def 1;
A12: [:f1,f2:] is being_homeomorphism by A10, A11, Th14;
consider h being Function of [:(Tdisk (Pn,r)),(Tdisk (Pm,s)):],(Tdisk ((0. (TOP-REAL (N + M))),1)) such that
A13: h is being_homeomorphism and
A14: h .: [:(Ball (Pn,r)),(Ball (Pm,s)):] = Ball ((0. (TOP-REAL (N + M))),1) by A1, A2, Th18;
A15: Tdisk (Pn,r) = (TOP-REAL N) | (cl_Ball (Pn,r)) by BROUWER:def 2;
then (Tdisk (Pn,r)) | BBn = (TOP-REAL N) | (Ball (Pn,r)) by A6, PRE_TOPC:7;
then A16: [:(Tdisk (Pn,r)),(Tdisk (Pm,s)):] | [:BBn,BBm:] = [:((TOP-REAL N) | Bn),((TOP-REAL M) | Bm):] by A5, BORSUK_3:22;
then reconsider h1 = h | [:BBn,BBm:] as Function of [:((TOP-REAL N) | Bn),((TOP-REAL M) | Bm):],((TOP-REAL (N + M)) | Bnm) by JORDAN24:12, A9, A14, A1, A15, A2, A4, A8;
reconsider hf = h1 * [:f1,f2:] as Function of [:T1,T2:],((TOP-REAL (N + M)) | Bnm) ;
h1 is being_homeomorphism by A9, A16, A13, A14, METRIZTS:2;
then hf is being_homeomorphism by A12, TOPS_2:57;
hence [:T1,T2:],(TOP-REAL (n + m)) | (Ball ((0. (TOP-REAL (n + m))),1)) are_homeomorphic by T_0TOPSP:def 1; :: thesis: verum