let M1, M2 be non empty TopSpace; ( M1 is locally_euclidean & M1,M2 are_homeomorphic implies M2 is locally_euclidean )
assume that
A1:
M1 is locally_euclidean
and
A2:
M1,M2 are_homeomorphic
; M2 is locally_euclidean
let p be Point of M2; MFOLD_0:def 2 ex U being a_neighborhood of p ex n being Nat st M2 | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
consider h being Function of M2,M1 such that
A3:
h is being_homeomorphism
by A2, T_0TOPSP:def 1;
reconsider hp = h . p as Point of M1 ;
consider U being a_neighborhood of hp, n being Nat such that
A4:
M1 | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
by A1;
A5:
rng h = [#] M1
by A3, TOPS_2:def 5;
then A6:
h .: (h " U) = U
by FUNCT_1:77;
then reconsider hhU = h | (h " U) as Function of (M2 | (h " U)),(M1 | U) by JORDAN24:12;
A7:
h " (Int U) c= h " U
by TOPS_1:16, RELAT_1:143;
hhU is being_homeomorphism
by A3, A6, METRIZTS:2;
then A8:
M2 | (h " U),M1 | U are_homeomorphic
by T_0TOPSP:def 1;
h " (Int U) is open
by A5, A3, TOPS_2:43;
then A9:
h " (Int U) c= Int (h " U)
by A7, TOPS_1:24;
A10:
dom h = [#] M2
by A3, TOPS_2:def 5;
hp in Int U
by CONNSP_2:def 1;
then
p in h " (Int U)
by FUNCT_1:def 7, A10;
then
h " U is a_neighborhood of p
by A9, CONNSP_2:def 1;
hence
ex U being a_neighborhood of p ex n being Nat st M2 | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
by A8, A4, BORSUK_3:3; verum