let n be Nat; for M1, M2 being non empty TopSpace st M1 is n -locally_euclidean & M2 is locally_euclidean & M1,M2 are_homeomorphic holds
M2 is n -locally_euclidean
let M1, M2 be non empty TopSpace; ( M1 is n -locally_euclidean & M2 is locally_euclidean & M1,M2 are_homeomorphic implies M2 is n -locally_euclidean )
assume that
A1:
M1 is n -locally_euclidean
and
A2:
M2 is locally_euclidean
and
A3:
M1,M2 are_homeomorphic
; M2 is n -locally_euclidean
consider h being Function of M1,M2 such that
A4:
h is being_homeomorphism
by A3, T_0TOPSP:def 1;
let q be Point of M2; MFOLD_0:def 3 ex U being a_neighborhood of q st M2 | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
set hp = q;
consider W being a_neighborhood of q, m being Nat such that
A5:
M2 | W, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic
by A2;
A6:
rng h = [#] M2
by A4, TOPS_2:def 5;
then A7:
not h " W is empty
by RELAT_1:139;
A8:
dom h = [#] M1
by A4, TOPS_2:def 5;
then consider p being object such that
A9:
p in [#] M1
and
A10:
h . p = q
by A6, FUNCT_1:def 3;
reconsider p = p as Point of M1 by A9;
consider U being a_neighborhood of p such that
A11:
M1 | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
by A1;
consider h2 being Function of (M2 | W),(Tdisk ((0. (TOP-REAL m)),1)) such that
A12:
h2 is being_homeomorphism
by T_0TOPSP:def 1, A5;
A13:
h .: (h " W) = W
by A6, FUNCT_1:77;
then reconsider hhW = h | (h " W) as Function of (M1 | (h " W)),(M2 | W) by JORDAN24:12;
hhW is being_homeomorphism
by A4, A13, METRIZTS:2;
then
h2 * hhW is being_homeomorphism
by A7, A12, TOPS_2:57;
then A14:
M1 | (h " W), Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic
by T_0TOPSP:def 1;
A15:
h " (Int W) c= h " W
by TOPS_1:16, RELAT_1:143;
h " (Int W) is open
by A6, A4, TOPS_2:43;
then A16:
h " (Int W) c= Int (h " W)
by A15, TOPS_1:24;
q in Int W
by CONNSP_2:def 1;
then A17:
p in h " (Int W)
by A10, FUNCT_1:def 7, A8;
p in Int U
by CONNSP_2:def 1;
then
n = m
by A17, A16, XBOOLE_0:3, A14, A11, BROUWER3:14;
hence
ex U being a_neighborhood of q st M2 | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
by A5; verum