let A be SetSequence of NAT; :: thesis: ( ( for n being Nat holds A . n = {n} ) implies for n being Nat holds (Partial_Union A) . n in Borel_Sets )
assume A0: for n being Nat holds A . n = {n} ; :: thesis: for n being Nat holds (Partial_Union A) . n in Borel_Sets
defpred S₁[ Nat] means (Partial_Union A) . $1 in Borel_Sets ;
S0: (Partial_Union A) . 0 = A . 0 by PROB_3:def 2;
(Partial_Union A) . 0 in Borel_Sets

proof

A . 0 = {0} by A0;
hence (Partial_Union A) . 0 in Borel_Sets by Th1, S0; :: thesis: verum

end;

then J0: S₁[ 0 ] ;
J1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume Q0: S₁[n] ; :: thesis: S₁[n + 1]
(Partial_Union A) . (n + 1) in Borel_Sets

proof

Q00: (Partial_Union A) . (n + 1) = ((Partial_Union A) . n) \/ (A . (n + 1)) by PROB_3:def 2;
{(n + 1)} in Borel_Sets by Th1;
then A . (n + 1) in Borel_Sets by A0;
hence (Partial_Union A) . (n + 1) in Borel_Sets by Q0, PROB_1:3, Q00; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds (Partial_Union A) . n in Borel_Sets

proof

for n being Nat holds S₁[n] from NAT_1:sch 2(J0, J1);
hence for n being Nat holds (Partial_Union A) . n in Borel_Sets ; :: thesis: verum

end;

hence for n being Nat holds (Partial_Union A) . n in Borel_Sets ; :: thesis: verum