reconsider nm = n + m as Nat ;
let p be Point of [:N,M:]; :: according to MFOLD_0:def 3 :: thesis: ex U being a_neighborhood of p st [:N,M:] | U, Tdisk ((0. (TOP-REAL (n + m))),1) are_homeomorphic
ex hf being Function of [:(Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL m)),1)):],(Tdisk ((0. (TOP-REAL (n + m))),1)) st
( hf is being_homeomorphism & hf .: [:(Ball ((0. (TOP-REAL n)),1)),(Ball ((0. (TOP-REAL m)),1)):] = Ball ((0. (TOP-REAL nm)),1) ) by TIETZE_2:19;
then A1: [:(Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL m)),1)):], Tdisk ((0. (TOP-REAL nm)),1) are_homeomorphic by T_0TOPSP:def 1;
p in the carrier of [:N,M:] ;
then p in [: the carrier of N, the carrier of M:] by BORSUK_1:def 2;
then consider x, y being object such that
A2: x in the carrier of N and
A3: y in the carrier of M and
A4: p = [x,y] by ZFMISC_1:def 2;
reconsider x = x as Point of N by A2;
consider Ux being a_neighborhood of x such that
A5: N | Ux, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def3;
reconsider y = y as Point of M by A3;
consider Uy being a_neighborhood of y such that
A6: M | Uy, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by Def3;
consider hy being Function of (M | Uy),(Tdisk ((0. (TOP-REAL m)),1)) such that
A7: hy is being_homeomorphism by A6, T_0TOPSP:def 1;
consider hx being Function of (N | Ux),(Tdisk ((0. (TOP-REAL n)),1)) such that
A8: hx is being_homeomorphism by A5, T_0TOPSP:def 1;
[:hx,hy:] is being_homeomorphism by A7, TIETZE_2:15, A8;
then A9: [:(N | Ux),(M | Uy):],[:(Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL m)),1)):] are_homeomorphic by T_0TOPSP:def 1;
[:(N | Ux),(M | Uy):] = [:N,M:] | [:Ux,Uy:] by BORSUK_3:22;
hence ex U being a_neighborhood of p st [:N,M:] | U, Tdisk ((0. (TOP-REAL (n + m))),1) are_homeomorphic by A1, A9, BORSUK_3:3, A4; :: thesis: verum