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₁( object ) -> set = { (Ball (x,(1 / (2 |^ (In ($1,NAT)))))) where x is Point of PM : x is Point of PM } ;
A4: for k being object st k in NAT holds
H₁(k) in bool (bool the carrier of T)

proof

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

proof

let B be object ; :: 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 ) ;
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
A5: for k being object 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;
A6: TopSpaceMetr PM = TopStruct(# the carrier of PM,(Family_open_set PM) #) by PCOMPS_1:def 5;
then A7: [#] T = [#] (TopSpaceMetr PM) by A2, PCOMPS_2:4;
A8: 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:

now :: thesis:

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

end;

then A9: FB . n is open ;
A10: [#] (TopSpaceMetr PM) c= union (FB . n)

proof

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

end;

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

proof

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

end;

then [#] (TopSpaceMetr PM) = union (FB . n) by A10;
then FB . n is Cover of T by A7, SETFAM_1:45;
then consider Un being FamilySequence of T such that
A16: ( Union Un is open & Union Un is Cover of T & Union Un is_finer_than FB . n & Un is sigma_discrete ) by A1, A9, 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 A16; :: thesis:

end;

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

proof

let k be object ; :: 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 object such that
A19: nm in dom PairFunc and
A20: k9 = PairFunc . nm by FUNCT_1:def 3;
consider n, m being object such that
A21: n in NAT and
A22: m in NAT and
A23: nm = [n,m] by A19, ZFMISC_1:def 2;
reconsider Unn = Un . n as FamilySequence of T by A21, FUNCT_2:5, FUNCT_2:66;
take Ux = Unn . m; :: thesis:
dom Unn = NAT by PARTFUN1:def 2;
then m in dom Unn by A22;
then Ux in rng Unn by FUNCT_1:3;
hence Ux in bool (bool the carrier of T) ; :: thesis:
let n1, m1 be Nat; :: thesis:
assume A24: PairFunc . [n1,m1] = k ; :: thesis:
reconsider nn1 = n1, mm1 = m1 as Element of NAT by ORDINAL1:def 12;

now :: thesis:

let Unn be FamilySequence of T; :: thesis:
assume A25: Unn = Un . nn1 ; :: thesis:
A26: [n,m] = [nn1,mm1] by A19, A20, A23, A24, Th2, FUNCT_2:19;
then n1 = n by XTUPLE_0:1;
hence Ux = Unn . mm1 by A25, A26, XTUPLE_0:1; :: thesis:

end;

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

end;

consider UX being sequence of (bool (bool the carrier of T)) such that
A27: for k being object st k in NAT holds
S₂[k,UX . k] from FUNCT_2:sch 1(A18);
A28: 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 A29: A in Family_open_set PM by A3, PRE_TOPC:def 2;
let p be Point of T; :: thesis:
assume A30: p in A ; :: thesis:
reconsider p = p as Element of PM by A30, A29;
consider r being Real such that
A31: r > 0 and
A32: Ball (p,r) c= A by A30, A29, PCOMPS_1:def 4;
consider n being Nat such that
A33: 1 / (2 |^ n) <= r by A31, PREPOWER:92;
consider Unn1 being FamilySequence of T such that
A34: Un . (n + 1) = Unn1 and
Union Unn1 is open and
A35: Union Unn1 is Cover of T and
A36: Union Unn1 is_finer_than FB . (n + 1) and
Unn1 is sigma_discrete by A17;
union (Union Unn1) = [#] T by A35, SETFAM_1:45;
then consider B being set such that
A37: p in B and
A38: B in Union Unn1 by TARSKI:def 4;
reconsider B = B as Subset of PM by A2, A38, PCOMPS_2:4;
consider B1 being set such that
A39: B1 in FB . (n + 1) and
A40: B c= B1 by A36, A38, SETFAM_1:def 2;
consider k being Nat such that
A41: B in Unn1 . k by A38, PROB_1:12;
( n + 1 = In ((n + 1),NAT) & B1 in H₁(n + 1) ) by A5, A39;
then consider q being Point of PM such that
A42: B1 = Ball (q,(1 / (2 |^ (n + 1)))) and
q is Element of PM ;

now :: thesis:

let s be Element of PM; :: thesis:
assume s in B ; :: thesis:
then A43: dist (q,s) < 1 / (2 |^ (n + 1)) by A40, A42, METRIC_1:11;
dist (q,p) < 1 / (2 |^ (n + 1)) by A37, A40, A42, 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 A43, 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 A33, XXREAL_0:2;
hence s in Ball (p,r) by METRIC_1:11; :: thesis:

end;

then A44: B c= Ball (p,r) ;
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
UX . (PairFunc . [(n + 1),kk]) = Unn1 . kk by A27, A34;
then B in Union UX by A41, PROB_1:12;
hence ex B being Subset of T st
( B in Union UX & p in B & B c= A ) by A32, A37, A44, XBOOLE_1:1; :: thesis:

end;

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

proof

let k be Nat; :: thesis:
A45: k in NAT by ORDINAL1:def 12;
NAT = rng PairFunc by Th2, FUNCT_2:def 3;
then consider nm being object such that
A46: nm in dom PairFunc and
A47: k = PairFunc . nm by FUNCT_1:def 3, A45;
consider n, m being object such that
A48: n in NAT and
A49: m in NAT and
A50: nm = [n,m] by A46, ZFMISC_1:def 2;
consider FS being FamilySequence of T such that
A51: Un . n = FS and
Union FS is open and
Union FS is Cover of T and
Union FS is_finer_than FB . n and
A52: FS is sigma_discrete by A17, A48;
dom FS = NAT by PARTFUN1:def 2;
then m in dom FS by A49;
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 A49, A52, NAGATA_1:def 2;
hence ( k is Element of NAT implies UX . k is discrete ) by A27, A47, A48, A49, A50, A51; :: thesis:

end;

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

proof

let UXk be object ; :: according to TARSKI:def 3 :: thesis:
assume UXk in Union UX ; :: thesis:
then consider k being Nat such that
A54: UXk in UX . k by PROB_1:12;
reconsider UXk9 = UXk as Subset of T by A54;
A55: k in NAT by ORDINAL1:def 12;
NAT = rng PairFunc by Th2, FUNCT_2:def 3;
then consider nm being object such that
A56: nm in dom PairFunc and
A57: k = PairFunc . nm by FUNCT_1:def 3, A55;
consider n, m being object 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 A27, A54, A57, A58, A59, A60, A55;
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 A17, A58;
then UXk9 is open by A61;
hence UXk in the topology of T by PRE_TOPC:def 2; :: thesis:

end;

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