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 A3, T_0TOPSP:def 1;

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. (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; :: thesis: verum

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 A3, T_0TOPSP:def 1;

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. (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; :: thesis: verum