A14:
[#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) = {(0. (TOP-REAL 0))}
by Lm2, EUCLID:22, EUCLID:77;

let M be non empty TopSpace; :: thesis: ( M is discrete implies M is 0 -locally_euclidean )

assume A15: M is discrete ; :: thesis: M is 0 -locally_euclidean

for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic

let M be non empty TopSpace; :: thesis: ( M is discrete implies M is 0 -locally_euclidean )

assume A15: M is discrete ; :: thesis: M is 0 -locally_euclidean

for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic

proof

hence
M is 0 -locally_euclidean
by Th13; :: thesis: verum
let p be Point of M; :: thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic

reconsider U = {p} as Subset of M by ZFMISC_1:31;

A16: ( U is open & p in U ) by A15, TARSKI:def 1, TDLAT_3:15;

then reconsider U = U as a_neighborhood of p by CONNSP_2:3;

take U ; :: thesis: U, [#] (TOP-REAL 0) are_homeomorphic

set f = {[p,(0. (TOP-REAL 0))]};

A17: p in [#] (M | U) by A16, PRE_TOPC:def 5;

A19: dom {[p,(0. (TOP-REAL 0))]} = U by RELAT_1:9;

then A20: dom {[p,(0. (TOP-REAL 0))]} = [#] (M | U) by PRE_TOPC:def 5;

then reconsider f = {[p,(0. (TOP-REAL 0))]} as Function of (M | U),((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A17, Lm2, ZFMISC_1:87, FUNCT_2:def 1, ZFMISC_1:31;

A21: rng f = [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A14, RELAT_1:9;

for P being Subset of (M | U) holds

( P is closed iff f .: P is closed )

hence U, [#] (TOP-REAL 0) are_homeomorphic by METRIZTS:def 1; :: thesis: verum

end;reconsider U = {p} as Subset of M by ZFMISC_1:31;

A16: ( U is open & p in U ) by A15, TARSKI:def 1, TDLAT_3:15;

then reconsider U = U as a_neighborhood of p by CONNSP_2:3;

take U ; :: thesis: U, [#] (TOP-REAL 0) are_homeomorphic

set f = {[p,(0. (TOP-REAL 0))]};

A17: p in [#] (M | U) by A16, PRE_TOPC:def 5;

A19: dom {[p,(0. (TOP-REAL 0))]} = U by RELAT_1:9;

then A20: dom {[p,(0. (TOP-REAL 0))]} = [#] (M | U) by PRE_TOPC:def 5;

then reconsider f = {[p,(0. (TOP-REAL 0))]} as Function of (M | U),((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A17, Lm2, ZFMISC_1:87, FUNCT_2:def 1, ZFMISC_1:31;

A21: rng f = [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A14, RELAT_1:9;

for P being Subset of (M | U) holds

( P is closed iff f .: P is closed )

proof

then
M | U,(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic
by T_0TOPSP:def 1, A20, A21, TOPS_2:58;
let P be Subset of (M | U); :: thesis: ( P is closed iff f .: P is closed )

end;per cases
( P is empty or not P is empty )
;

end;

suppose A23:
not P is empty
; :: thesis: ( P is closed iff f .: P is closed )

then
P = [#] (M | U)
by A20, A19, ZFMISC_1:33;

hence ( P is closed implies f .: P is closed ) by A21, A20, RELAT_1:113; :: thesis: ( f .: P is closed implies P is closed )

thus ( f .: P is closed implies P is closed ) by A23, A20, A19, ZFMISC_1:33; :: thesis: verum

end;hence ( P is closed implies f .: P is closed ) by A21, A20, RELAT_1:113; :: thesis: ( f .: P is closed implies P is closed )

thus ( f .: P is closed implies P is closed ) by A23, A20, A19, ZFMISC_1:33; :: thesis: verum

hence U, [#] (TOP-REAL 0) are_homeomorphic by METRIZTS:def 1; :: thesis: verum