let p be Point of [:N,M:]; :: according to MFOLD_0:def 2 :: thesis: 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; :: thesis: verum