let n be Nat; :: thesis: 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; :: thesis: ( 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 ; :: thesis: M2 is n -locally_euclidean
consider h being Function of M1,M2 such that
A4: h is being_homeomorphism by ;
let q be Point of M2; :: according to MFOLD_0:def 3 :: thesis: ex U being a_neighborhood of q st M2 | U, Tdisk ((0. ()),1) are_homeomorphic
set hp = q;
consider W being a_neighborhood of q, m being Nat such that
A5: M2 | W, Tdisk ((0. ()),1) are_homeomorphic by A2;
A6: rng h = [#] M2 by ;
then A7: not h " W is empty by RELAT_1:139;
A8: dom h = [#] M1 by ;
then consider p being object such that
A9: p in [#] M1 and
A10: h . p = q by ;
reconsider p = p as Point of M1 by A9;
consider U being a_neighborhood of p such that
A11: M1 | U, Tdisk ((0. ()),1) are_homeomorphic by A1;
consider h2 being Function of (M2 | W),(Tdisk ((0. ()),1)) such that
A12: h2 is being_homeomorphism by ;
A13: h .: (h " W) = W by ;
then reconsider hhW = h | (h " W) as Function of (M1 | (h " W)),(M2 | W) by JORDAN24:12;
hhW is being_homeomorphism by ;
then h2 * hhW is being_homeomorphism by ;
then A14: M1 | (h " W), Tdisk ((0. ()),1) are_homeomorphic by T_0TOPSP:def 1;
A15: h " (Int W) c= h " W by ;
h " (Int W) is open by ;
then A16: h " (Int W) c= Int (h " W) by ;
q in Int W by CONNSP_2:def 1;
then A17: p in h " (Int W) by ;
p in Int U by CONNSP_2:def 1;
then n = m by ;
hence ex U being a_neighborhood of q st M2 | U, Tdisk ((0. ()),1) are_homeomorphic by A5; :: thesis: verum