let n be Nat; :: thesis:
let T be TopSpace; :: thesis:
let g be SetSequence of T; :: thesis:
assume A1: for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ; :: thesis:
defpred S₁[ object , object ] means for n being Nat
for F being Subset-Family of T st n = $1 & F = $2 holds
( union F = g . n & F is closed & F is countable );
A2: for x being object st x in NAT holds
ex y being object st
( y in bool (bool the carrier of T) & S₁[x,y] )

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Element of NAT ;
g . n is F_sigma by A1;
then consider y being closed countable Subset-Family of T such that
A3: g . n = union y by TOPGEN_4:def 6;
take y ; :: thesis:
thus ( y in bool (bool the carrier of T) & S₁[x,y] ) by A3; :: thesis:

end;

consider f being SetSequence of (bool the carrier of T) such that
A4: for x being object st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
take F = Union f; :: thesis:
thus F is closed :: thesis:

let A be Subset of T; :: according to TOPS_2:def 2 :: thesis:
assume A in F ; :: thesis:
then consider n being Nat such that
A5: A in f . n by PROB_1:12;
n in NAT by ORDINAL1:def 12;
then f . n is closed by A4;
hence A is closed by A5; :: thesis:

end;

for A being Subset of T st A in F holds
( A is finite-ind & ind A <= n )

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Union g ; :: thesis:
then consider i being Nat such that
A10: x in g . i by PROB_1:12;
i in NAT by ORDINAL1:def 12;
then union (f . i) = g . i by A4;
then consider y being set such that
A11: x in y and
A12: y in f . i by A10, TARSKI:def 4;
y in F by A12, PROB_1:12;
hence x in union F by A11, TARSKI:def 4; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union F ; :: thesis:
then consider y being set such that
A13: x in y and
A14: y in F by TARSKI:def 4;
consider i being Nat such that
A15: y in f . i by A14, PROB_1:12;
i in NAT by ORDINAL1:def 12;
then union (f . i) = g . i by A4;
then x in g . i by A13, A15, TARSKI:def 4;
hence x in Union g by PROB_1:12; :: thesis:

end;