A2: [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) = {(0. (TOP-REAL 0))} by EUCLID:25, JORDAN2C:113, A1;
let M be non empty TopSpace; :: thesis: ( M is discrete implies M is 0 -locally_euclidean )
assume A16: 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

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:37;
A17: ( U is open & p in U ) by A16, TDLAT_3:17, TARSKI:def 1;
then reconsider U = U as a_neighborhood of p by CONNSP_2:5;
take U ; :: thesis: U, [#] (TOP-REAL 0) are_homeomorphic
set f = {[p,(0. (TOP-REAL 0))]};
A18: p in [#] (M | U) by A17, PRE_TOPC:def 10;
A19: [p,(0. (TOP-REAL 0))] in [: the carrier of (M | U), the carrier of ((TOP-REAL 0) | ([#] (TOP-REAL 0))):] by A18, ZFMISC_1:106, A1;
A20: dom {[p,(0. (TOP-REAL 0))]} = U by RELAT_1:23;
then A21: dom {[p,(0. (TOP-REAL 0))]} = [#] (M | U) by PRE_TOPC:def 10;
then reconsider f = {[p,(0. (TOP-REAL 0))]} as Function of (M | U),((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A19, FUNCT_2:def 1, ZFMISC_1:37;
A22: rng f = [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A2, RELAT_1:23;
for P being Subset of (M | U) holds
( P is closed iff f .: P is closed )

proof

let P be Subset of (M | U); :: thesis: ( P is closed iff f .: P is closed )

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

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

then f .: P is empty by RELAT_1:149;
hence ( P is closed iff f .: P is closed ) by A23; :: thesis: verum

end;

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

then P = [#] (M | U) by A21, ZFMISC_1:39, A20;
hence ( P is closed implies f .: P is closed ) by A22, A21, RELAT_1:146; :: thesis: ( f .: P is closed implies P is closed )
thus ( f .: P is closed implies P is closed ) by A24, A21, ZFMISC_1:39, A20; :: thesis: verum

end;

end;

end;

then f is being_homeomorphism by A21, A22, TOPS_2:72;
then M | U,(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic by T_0TOPSP:def 1;
hence U, [#] (TOP-REAL 0) are_homeomorphic by METRIZTS:def 1; :: thesis: verum

end;

hence M is 0 -locally_euclidean by Th15; :: thesis: verum