for n being Nat holds (GoCross_Seq_REAL (pm,k)) . n is Event of Borel_Sets

proof

let n be Nat; :: thesis: (GoCross_Seq_REAL (pm,k)) . n is Event of Borel_Sets
{((pm * k) * ((n + 1) "))} in Borel_Sets by Th1;
hence (GoCross_Seq_REAL (pm,k)) . n is Event of Borel_Sets by Def4; :: thesis: verum

end;

hence GoCross_Seq_REAL (pm,k) is SetSequence of Borel_Sets by PROB_1:25; :: thesis: verum