defpred S₁[ set ] means (Intersect_Shift_Seq A) . $1 is Event of Sigma;
for n being Element of NAT holds (Complement (@Shift_Seq (A,0))) . n is Event of Sigma

proof

let n be Element of NAT ; :: thesis: (Complement (@Shift_Seq (A,0))) . n is Event of Sigma
((@Shift_Seq (A,0)) . n) ` is Event of Sigma by PROB_1:50;
hence (Complement (@Shift_Seq (A,0))) . n is Event of Sigma by PROB_1:def 4; :: thesis: verum

end;

then A1: Complement (@Shift_Seq (A,0)) is SetSequence of Sigma by PROB_1:57;
A2: Union (Complement (@Shift_Seq (A,0))) is Event of Sigma by A1, PROB_1:58;
(Intersect_Shift_Seq A) . 0 = Intersection (@Shift_Seq (A,0)) by Def12;
then A3: S₁[ 0 ] by A2, PROB_1:50;
A4: 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 (Intersect_Shift_Seq A) . k is Event of Sigma ; :: thesis: S₁[k + 1]
for n being Element of NAT holds (Complement (@Shift_Seq (A,(k + 1)))) . n is Event of Sigma

proof

let n be Element of NAT ; :: thesis: (Complement (@Shift_Seq (A,(k + 1)))) . n is Event of Sigma
((@Shift_Seq (A,(k + 1))) . n) ` is Event of Sigma by PROB_1:50;
hence (Complement (@Shift_Seq (A,(k + 1)))) . n is Event of Sigma by PROB_1:def 4; :: thesis: verum

end;

then A5: Complement (@Shift_Seq (A,(k + 1))) is SetSequence of Sigma by PROB_1:57;
A6: Union (Complement (@Shift_Seq (A,(k + 1)))) is Event of Sigma by A5, PROB_1:58;
(Intersect_Shift_Seq A) . (k + 1) = Intersection (@Shift_Seq (A,(k + 1))) by Def12;
hence S₁[k + 1] by A6, PROB_1:50; :: thesis: verum

end;

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