defpred S₁[ Nat] means (GoCross_Union pm) . $1 is Event of Borel_Sets ;
Union (GoCross_Partial_Union (pm,0)) is Event of Borel_Sets by PROB_1:17;
then J1: S₁[ 0 ] by Def6;
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: Union (GoCross_Partial_Union (pm,(n + 1))) is Event of Borel_Sets by PROB_1:17;
((GoCross_Union pm) . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) is Event of Borel_Sets by B1, C2, PROB_1:21;
hence S₁[n + 1] by Def6; :: thesis: verum

end;

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