consider A being SetSequence of Borel_Sets such that
Q10: for n being Nat holds A . n = {n} by Q0;
reconsider A = A as SetSequence of REAL ;
Union A = NAT

proof

for x being object holds
( x in Union A iff x in NAT )

proof

let x be object ; :: thesis: ( x in Union A iff x in NAT )
H0: for n being Element of NAT
for x being object holds
( x in {n} iff x = n ) by TARSKI:def 1;
H1: ( ex n being Nat st x in A . n implies ex n being Element of NAT st x in A . n )

proof

given n being Nat such that C0: x in A . n ; :: thesis: ex n being Element of NAT st x in A . n
n + 0 in NAT ;
then consider n being Element of NAT such that
C1: x in A . n by C0;
thus ex n being Element of NAT st x in A . n by C1; :: thesis: verum

end;

thus ( x in Union A implies x in NAT ) :: thesis: ( x in NAT implies x in Union A )

proof

assume C0: x in Union A ; :: thesis: x in NAT
ex n being Element of NAT st
( x in A . n & A . n = {n} )

proof

consider n being Element of NAT such that
D0: x in A . n by C0, PROB_1:12, H1;
A . n = {n} by Q10;
hence ex n being Element of NAT st
( x in A . n & A . n = {n} ) by D0; :: thesis: verum

end;

then ex n being Element of NAT st x = n by H0;
hence x in NAT ; :: thesis: verum

end;

assume C000: x in NAT ; :: thesis: x in Union A
ex k being Nat st
( x in {k} & A . k = {k} )

proof

reconsider k = x as Nat by C000;
A: x in {k} by TARSKI:def 1;
A . k = {k} by Q10;
hence ex k being Nat st
( x in {k} & A . k = {k} ) by A; :: thesis: verum

end;

hence x in Union A by PROB_1:12; :: thesis: verum

end;

hence Union A = NAT ; :: thesis: verum

end;

hence NAT is Event of Borel_Sets by PROB_1:17; :: thesis: verum