defpred S₁[ set ] means (Intersect_Shift_Seq A) . Omega is Event of Sigma;
A2: Union (Complement (A ^\ 0)) is Event of Sigma by PROB_1:26;
(Intersect_Shift_Seq A) . 0 = Intersection (A ^\ 0) by Def12;
then A3: S₁[ 0 ] by A2, PROB_1:20;
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]
A6: Union (Complement (A ^\ (k + 1))) is Event of Sigma by PROB_1:26;
(Intersect_Shift_Seq A) . (k + 1) = Intersection (A ^\ (k + 1)) by Def12;
hence S₁[k + 1] by A6, PROB_1:20; :: 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 Sigma -valued by PROB_1:25; :: thesis: verum