defpred S₁[ set ] means (Shift_Seq (A,s)) . $1 is Event of Sigma;
A1: (Shift_Seq (A,s)) . 0 = A . (0 + s) by NAT_1:def 3;
A2: S₁[ 0 ] by A1;
A3: 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 (Shift_Seq (A,s)) . k is Event of Sigma ; :: thesis: S₁[k + 1]
A . (s + (k + 1)) is Event of Sigma ;
hence S₁[k + 1] by NAT_1:def 3; :: thesis: verum

end;

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