defpred S₁[ Nat] means (GoCross_Partial_Union (pm,k)) . $1 is Event of Borel_Sets ;
(GoCross_Seq_REAL (pm,k)) . 0 is Event of Borel_Sets by PROB_1:25;
then J1: S₁[ 0 ] by Def5;
J2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B1: S₁[n] ; :: thesis: S₁[n + 1]
C2: (GoCross_Seq_REAL (pm,k)) . (n + 1) is Event of Borel_Sets by PROB_1:25;
((GoCross_Partial_Union (pm,k)) . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) is Event of Borel_Sets by B1, C2, PROB_1:21;
hence S₁[n + 1] by Def5; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J1, J2);
hence GoCross_Partial_Union (pm,k) is SetSequence of Borel_Sets by PROB_1:25; :: thesis: verum