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