let T be non empty TopSpace; :: thesis: ( T is metrizable implies ex Un being FamilySequence of T st Un is Basis_sigma_discrete )
assume A1: T is metrizable ; :: thesis: ex Un being FamilySequence of T st Un is Basis_sigma_discrete
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 ;
set bbcT = bool (bool the carrier of T);
reconsider PM = SpaceMetr ( the carrier of T,metr) as non empty MetrSpace by ;
deffunc H1( 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
H1(k) in bool (bool the carrier of T)
proof
let k be object ; :: thesis: ( k in NAT implies H1(k) in bool (bool the carrier of T) )
assume k in NAT ; :: thesis: H1(k) in bool (bool the carrier of T)
then reconsider k = k as Element of NAT ;
H1(k) c= bool the carrier of T
proof
let B be object ; :: according to TARSKI:def 3 :: thesis: ( not B in H1(k) or B in bool the carrier of T )
assume B in H1(k) ; :: thesis: B in bool the carrier of T
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: verum
end;
hence H1(k) in bool (bool the carrier of T) ; :: thesis: verum
end;
consider FB being FamilySequence of T such that
A5: for k being object st k in NAT holds
FB . k = H1(k) from defpred S1[ 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,() #) by PCOMPS_1:def 5;
then A7: [#] T = [#] () by ;
A8: for n being Element of NAT ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S1[n,Un]
proof
let n be Element of NAT ; :: thesis: ex Un being Element of Funcs (NAT,(bool (bool the carrier of T))) st S1[n,Un]
now :: thesis: for U being Subset of T st U in FB . n holds
U is open
let U be Subset of T; :: thesis: ( U in FB . n implies U is open )
assume U in FB . n ; :: thesis: U is open
then U in H1(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 ;
hence U is open by PRE_TOPC:def 2; :: thesis: verum
end;
then A9: FB . n is open ;
A10: [#] () c= union (FB . n)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] () or x in union (FB . n) )
assume x in [#] () ; :: thesis: x in union (FB . n)
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 ;
Ball (x9,(1 / (2 |^ n))) in H1(n) ;
then Ball (x9,(1 / (2 |^ n))) in FB . n by A5;
hence x in union (FB . n) by ; :: thesis: verum
end;
union (FB . n) c= [#] ()
proof
given x being object such that A12: x in union (FB . n) and
A13: not x in [#] () ; :: according to TARSKI:def 3 :: thesis: contradiction
consider A being set such that
A14: x in A and
A15: A in FB . n by ;
A in H1(n) by ;
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: verum
end;
then [#] () = union (FB . n) by A10;
then FB . n is Cover of T by ;
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 S1[n,Un] by A16; :: thesis: verum
end;
consider Un being sequence of (Funcs (NAT,(bool (bool the carrier of T)))) such that
A17: for n being Element of NAT holds S1[n,Un . n] from defpred S2[ 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) & S2[k,Ux] )
proof
let k be object ; :: thesis: ( k in NAT implies ex Ux being object st
( Ux in bool (bool the carrier of T) & S2[k,Ux] ) )

assume k in NAT ; :: thesis: ex Ux being object st
( Ux in bool (bool the carrier of T) & S2[k,Ux] )

then reconsider k9 = k as Element of NAT ;
NAT = rng PairFunc by ;
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 ;
reconsider Unn = Un . n as FamilySequence of T by ;
take Ux = Unn . m; :: thesis: ( Ux in bool (bool the carrier of T) & S2[k,Ux] )
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: S2[k,Ux]
let n1, m1 be Nat; :: thesis: ( PairFunc . [n1,m1] = k implies for Unn being FamilySequence of T st Unn = Un . n1 holds
Ux = Unn . m1 )

assume A24: PairFunc . [n1,m1] = k ; :: thesis: for Unn being FamilySequence of T st Unn = Un . n1 holds
Ux = Unn . m1

reconsider nn1 = n1, mm1 = m1 as Element of NAT by ORDINAL1:def 12;
now :: thesis: for Unn being FamilySequence of T st Unn = Un . nn1 holds
Ux = Unn . mm1
let Unn be FamilySequence of T; :: thesis: ( Unn = Un . nn1 implies Ux = Unn . mm1 )
assume A25: Unn = Un . nn1 ; :: thesis: Ux = Unn . mm1
A26: [n,m] = [nn1,mm1] by ;
then n1 = n by XTUPLE_0:1;
hence Ux = Unn . mm1 by ; :: thesis: verum
end;
hence for Unn being FamilySequence of T st Unn = Un . n1 holds
Ux = Unn . m1 ; :: thesis: verum
end;
consider UX being sequence of (bool (bool the carrier of T)) such that
A27: for k being object st k in NAT holds
S2[k,UX . k] from 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: ( A is open implies 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 ) )

assume A is open ; :: thesis: 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 )

then A29: A in Family_open_set PM by ;
let p be Point of T; :: thesis: ( p in A implies ex B being Subset of T st
( B in Union UX & p in B & B c= A ) )

assume A30: p in A ; :: thesis: ex B being Subset of T st
( B in Union UX & p in B & B c= A )

reconsider p = p as Element of PM by ;
consider r being Real such that
A31: r > 0 and
A32: Ball (p,r) c= A by ;
consider n being Nat such that
A33: 1 / (2 |^ n) <= r by ;
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 ;
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 ;
consider B1 being set such that
A39: B1 in FB . (n + 1) and
A40: B c= B1 by ;
consider k being Nat such that
A41: B in Unn1 . k by ;
( n + 1 = In ((n + 1),NAT) & B1 in H1(n + 1) ) by ;
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: for s being Element of PM st s in B holds
s in Ball (p,r)
let s be Element of PM; :: thesis: ( s in B implies s in Ball (p,r) )
assume s in B ; :: thesis: s in Ball (p,r)
then A43: dist (q,s) < 1 / (2 |^ (n + 1)) by ;
dist (q,p) < 1 / (2 |^ (n + 1)) by ;
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 ;
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 ;
hence s in Ball (p,r) by METRIC_1:11; :: thesis: verum
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 ;
then B in Union UX by ;
hence ex B being Subset of T st
( B in Union UX & p in B & B c= A ) by ; :: thesis: verum
end;
for k being Element of NAT holds UX . k is discrete
proof
let k be Nat; :: thesis: ( k is Element of NAT implies UX . k is discrete )
A45: k in NAT by ORDINAL1:def 12;
NAT = rng PairFunc by ;
then consider nm being object such that
A46: nm in dom PairFunc and
A47: k = PairFunc . nm by ;
consider n, m being object such that
A48: n in NAT and
A49: m in NAT and
A50: nm = [n,m] by ;
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 ;
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 ;
hence ( k is Element of NAT implies UX . k is discrete ) by A27, A47, A48, A49, A50, A51; :: thesis: verum
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: ( not UXk in Union UX or UXk in the topology of T )
assume UXk in Union UX ; :: thesis: UXk in the topology of T
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 ;
then consider nm being object such that
A56: nm in dom PairFunc and
A57: k = PairFunc . nm by ;
consider n, m being object such that
A58: n in NAT and
A59: m in NAT and
A60: nm = [n,m] by ;
reconsider Unn = Un . n as FamilySequence of T by ;
UXk in Unn . m by A27, A54, A57, A58, A59, A60, A55;
then A61: UXk in Union Unn by ;
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 ;
then UXk9 is open by A61;
hence UXk in the topology of T by PRE_TOPC:def 2; :: thesis: verum
end;
then Union UX is Basis of T by ;
then UX is Basis_sigma_discrete by ;
hence ex Un being FamilySequence of T st Un is Basis_sigma_discrete ; :: thesis: verum