reconsider nm = n + m as Nat ;
let p be Point of [:N,M:]; MFOLD_0:def 3 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; verum