defpred S₁[ set ] means (Union_Shift_Seq A) . $1 is Event of Sigma;
(Union_Shift_Seq A) . 0 = Union (@Shift_Seq (A,0)) by Def9;
then A1: S₁[ 0 ] by PROB_1:46;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume (Union_Shift_Seq A) . k is Event of Sigma ; :: thesis: S₁[k + 1]
Union (@Shift_Seq (A,(k + 1))) in Sigma by PROB_1:46;
hence S₁[k + 1] by Def9; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
hence Union_Shift_Seq A is SetSequence of Sigma by PROB_1:57; :: thesis: verum