let T be non empty TopSpace; :: thesis:
assume A1: T is metrizable ; :: thesis:
consider metr being Function of [: the carrier of T, the carrier of T:],REAL such that
A2: metr is_metric_of the carrier of T and
A3: Family_open_set (SpaceMetr ( the carrier of T,metr)) = the topology of T by A1, PCOMPS_1:def 8;
set bbcT = bool (bool the carrier of T);
reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by A2, PCOMPS_1:36;
deffunc H₁( set ) -> set = { (Ball (x,(1 / (2 |^ (In ($1,NAT)))))) where x is Point of PM : x is Point of PM } ;
A4: for k being set st k in NAT holds
H₁(k) in bool (bool the carrier of T)

proof

let k be set ; :: thesis:
assume k in NAT ; :: thesis:
then reconsider k = k as Element of NAT ;
H₁(k) c= bool the carrier of T

proof

A5: In (k,NAT) = k by FUNCT_7:def 1;
let B be set ; :: according to TARSKI:def 3 :: thesis:
assume B in H₁(k) ; :: thesis:
then ex x being Point of PM st
( B = Ball (x,(1 / (2 |^ k))) & x is Point of PM ) by A5;
then B in Family_open_set PM by PCOMPS_1:29;
hence B in bool the carrier of T by A3; :: thesis:

end;

hence H₁(k) in bool (bool the carrier of T) ; :: thesis:

end;

consider FB being FamilySequence of T such that
A6: for k being set st k in NAT holds
FB . k = H₁(k) from FUNCT_2:sch 2(A4);
defpred S₁[ set , set ] means ex FS being FamilySequence of T st
( $2 = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . $1 & FS is sigma_discrete );
set TPM = TopSpaceMetr PM;
A7: TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #) by PCOMPS_1:def 5;
then A8: [#] T = [#] (TopSpaceMetr PM) by A2, PCOMPS_2:4;
A9: for n being Element of NAT ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S₁[n,Un]

proof

let n be Element of NAT ; :: thesis:
A10: n = In (n,NAT) by FUNCT_7:def 1;

now

let U be Subset of T; :: thesis:
assume U in FB . n ; :: thesis:
then U in H₁(n) by A6;
then ex x being Point of PM st
( U = Ball (x,(1 / (2 |^ n))) & x is Point of PM ) by A10;
then U in the topology of T by A3, PCOMPS_1:29;
hence U is open by PRE_TOPC:def 2; :: thesis:

end;

then A11: FB . n is open by TOPS_2:def 1;
A12: [#] (TopSpaceMetr PM) c= union (FB . n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in [#] (TopSpaceMetr PM) ; :: thesis:
then reconsider x9 = x as Element of PM by A7;
2 |^ n > 0 by NEWTON:83;
then A13: x9 in Ball (x9,(1 / (2 |^ n))) by TBSP_1:11, XREAL_1:139;
Ball (x9,(1 / (2 |^ n))) in H₁(n) by A10;
then Ball (x9,(1 / (2 |^ n))) in FB . n by A6;
hence x in union (FB . n) by A13, TARSKI:def 4; :: thesis:

end;

union (FB . n) c= [#] (TopSpaceMetr PM)

proof

given x being set such that A14: x in union (FB . n) and
A15: not x in [#] (TopSpaceMetr PM) ; :: according to TARSKI:def 3 :: thesis:
consider A being set such that
A16: x in A and
A17: A in FB . n by A14, TARSKI:def 4;
A in H₁(n) by A6, A17;
then ex y being Point of PM st
( A = Ball (y,(1 / (2 |^ n))) & y is Point of PM ) by A10;
hence contradiction by A7, A15, A16; :: thesis:

end;

then [#] (TopSpaceMetr PM) = union (FB . n) by A12, XBOOLE_0:def 10;
then FB . n is Cover of T by A8, SETFAM_1:45;
then consider Un being FamilySequence of T such that
A18: ( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FB . n & Un is sigma_discrete ) by A1, A11, Th20;
Un in Funcs (NAT,(bool (bool the carrier of T))) by FUNCT_2:8;
hence ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S₁[n,Un] by A18; :: thesis:

end;

consider Un being Function of NAT,(Funcs (NAT,(bool (bool the carrier of T)))) such that
A19: for n being Element of NAT holds S₁[n,Un . n] from FUNCT_2:sch 3(A9);
defpred S₂[ set , set ] means for n, m being Element of NAT st PairFunc . [n,m] = $1 holds
for Unn being FamilySequence of T st Unn = Un . n holds
$2 = Unn . m;
A20: for k being set st k in NAT holds
ex Ux being set st
( Ux in bool (bool the carrier of T) & S₂[k,Ux] )

proof

let k be set ; :: thesis:
assume k in NAT ; :: thesis:
then reconsider k9 = k as Element of NAT ;
NAT = rng PairFunc by Th2, FUNCT_2:def 3;
then consider nm being set such that
A21: nm in dom PairFunc and
A22: k9 = PairFunc . nm by FUNCT_1:def 3;
consider n, m being set such that
A23: n in NAT and
A24: m in NAT and
A25: nm = [n,m] by A21, ZFMISC_1:def 2;
reconsider Unn = Un . n as FamilySequence of T by A23, FUNCT_2:5, FUNCT_2:66;
take Ux = Unn . m; :: thesis:
dom Unn = NAT by PARTFUN1:def 2;
then m in dom Unn by A24;
then Ux in rng Unn by FUNCT_1:3;
hence Ux in bool (bool the carrier of T) ; :: thesis:

now

let n1, m1 be Element of NAT ; :: thesis:
assume A26: PairFunc . [n1,m1] = k ; :: thesis:

now

let Unn be FamilySequence of T; :: thesis:
assume A27: Unn = Un . n1 ; :: thesis:
A28: [n,m] = [n1,m1] by A21, A22, A25, A26, Th2, FUNCT_2:19;
then n1 = n by ZFMISC_1:27;
hence Ux = Unn . m1 by A27, A28, ZFMISC_1:27; :: thesis:

end;

hence for Unn being FamilySequence of T st Unn = Un . n1 holds
Ux = Unn . m1 ; :: thesis:

end;

hence S₂[k,Ux] ; :: thesis:

end;

consider UX being Function of NAT,(bool (bool the carrier of T)) such that
A29: for k being set st k in NAT holds
S₂[k,UX . k] from FUNCT_2:sch 1(A20);
A30: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex B being Subset of T st
( B in Union UX & p in B & B c= A )

proof

let A be Subset of T; :: thesis:
assume A is open ; :: thesis:
then A31: A in Family_open_set PM by A3, PRE_TOPC:def 2;
let p be Point of T; :: thesis:
assume A32: p in A ; :: thesis:
reconsider p = p as Element of PM by A32, A31;
consider r being Real such that
A33: r > 0 and
A34: Ball (p,r) c= A by A32, A31, PCOMPS_1:def 4;
consider n being Element of NAT such that
A35: 1 / (2 |^ n) <= r by A33, PREPOWER:92;
consider Unn1 being FamilySequence of T such that
A36: Un . (n + 1) = Unn1 and
Union Unn1 is open and
A37: Union Unn1 is Cover of T and
A38: Union Unn1 is_finer_than FB . (n + 1) and
Unn1 is sigma_discrete by A19;
union (Union Unn1) = [#] T by A37, SETFAM_1:45;
then consider B being set such that
A39: p in B and
A40: B in Union Unn1 by TARSKI:def 4;
reconsider B = B as Subset of PM by A2, A40, PCOMPS_2:4;
consider B1 being set such that
A41: B1 in FB . (n + 1) and
A42: B c= B1 by A38, A40, SETFAM_1:def 2;
consider k being Element of NAT such that
A43: B in Unn1 . k by A40, PROB_1:12;
( n + 1 = In ((n + 1),NAT) & B1 in H₁(n + 1) ) by A6, A41, FUNCT_7:def 1;
then consider q being Point of PM such that
A44: B1 = Ball (q,(1 / (2 |^ (n + 1)))) and
q is Element of PM ;

now

let s be Element of PM; :: thesis:
assume s in B ; :: thesis:
then A45: dist (q,s) < 1 / (2 |^ (n + 1)) by A42, A44, METRIC_1:11;
dist (q,p) < 1 / (2 |^ (n + 1)) by A39, A42, A44, METRIC_1:11;
then ( dist (p,s) <= (dist (q,p)) + (dist (q,s)) & (dist (q,p)) + (dist (q,s)) < (1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) ) by A45, METRIC_1:4, XREAL_1:8;
then dist (p,s) < 2 * (1 / (2 |^ (n + 1))) by XXREAL_0:2;
then dist (p,s) < (1 / ((2 |^ n) * 2)) * 2 by NEWTON:6;
then dist (p,s) < 1 / (2 |^ n) by XCMPLX_1:92;
then dist (p,s) < r by A35, XXREAL_0:2;
hence s in Ball (p,r) by METRIC_1:11; :: thesis:

end;

then A46: B c= Ball (p,r) by SUBSET_1:2;
UX . (PairFunc . [(n + 1),k]) = Unn1 . k by A29, A36;
then B in Union UX by A43, PROB_1:12;
hence ex B being Subset of T st
( B in Union UX & p in B & B c= A ) by A34, A39, A46, XBOOLE_1:1; :: thesis:

end;

for k being Element of NAT holds UX . k is discrete

proof

let k be Element of NAT ; :: thesis:
NAT = rng PairFunc by Th2, FUNCT_2:def 3;
then consider nm being set such that
A47: nm in dom PairFunc and
A48: k = PairFunc . nm by FUNCT_1:def 3;
consider n, m being set such that
A49: n in NAT and
A50: m in NAT and
A51: nm = [n,m] by A47, ZFMISC_1:def 2;
consider FS being FamilySequence of T such that
A52: Un . n = FS and
Union FS is open and
Union FS is Cover of T and
Union FS is_finer_than FB . n and
A53: FS is sigma_discrete by A19, A49;
dom FS = NAT by PARTFUN1:def 2;
then m in dom FS by A50;
then FS . m in rng FS by FUNCT_1:3;
then FS . m in bool (bool the carrier of T) ;
then reconsider FSm = FS . m as Subset-Family of T ;
FSm is discrete by A50, A53, NAGATA_1:def 2;
hence UX . k is discrete by A29, A48, A49, A50, A51, A52; :: thesis:

end;

then A54: UX is sigma_discrete by NAGATA_1:def 2;
Union UX c= the topology of T

proof

let UXk be set ; :: according to TARSKI:def 3 :: thesis:
assume UXk in Union UX ; :: thesis:
then consider k being Element of NAT such that
A55: UXk in UX . k by PROB_1:12;
reconsider UXk9 = UXk as Subset of T by A55;
NAT = rng PairFunc by Th2, FUNCT_2:def 3;
then consider nm being set such that
A56: nm in dom PairFunc and
A57: k = PairFunc . nm by FUNCT_1:def 3;
consider n, m being set such that
A58: n in NAT and
A59: m in NAT and
A60: nm = [n,m] by A56, ZFMISC_1:def 2;
reconsider Unn = Un . n as FamilySequence of T by A58, FUNCT_2:5, FUNCT_2:66;
UXk in Unn . m by A29, A55, A57, A58, A59, A60;
then A61: UXk in Union Unn by A59, PROB_1:12;
ex FS being FamilySequence of T st
( Un . n = FS & Union FS is open & Union FS is Cover of T & Union FS is_finer_than FB . n & FS is sigma_discrete ) by A19, A58;
then UXk9 is open by A61, TOPS_2:def 1;
hence UXk in the topology of T by PRE_TOPC:def 2; :: thesis:

end;

then Union UX is Basis of T by A30, YELLOW_9:32;
then UX is Basis_sigma_discrete by A54, NAGATA_1:def 5;
hence ex Un being FamilySequence of T st Un is Basis_sigma_discrete ; :: thesis: