defpred S_{1}[ set ] means (Union_Shift_Seq A) . Omega is Event of Sigma;

(Union_Shift_Seq A) . 0 = Union (A ^\ 0) by Def7;

then A1: S_{1}[ 0 ]
by PROB_1:17;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A1, A2);

hence Union_Shift_Seq A is Sigma -valued by PROB_1:25; :: thesis: verum

(Union_Shift_Seq A) . 0 = Union (A ^\ 0) by Def7;

then A1: S

A2: for k being Nat st S

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume (Union_Shift_Seq A) . k is Event of Sigma ; :: thesis: S_{1}[k + 1]

Union (A ^\ (k + 1)) in Sigma by PROB_1:17;

hence S_{1}[k + 1]
by Def7; :: thesis: verum

end;assume (Union_Shift_Seq A) . k is Event of Sigma ; :: thesis: S

Union (A ^\ (k + 1)) in Sigma by PROB_1:17;

hence S

hence Union_Shift_Seq A is Sigma -valued by PROB_1:25; :: thesis: verum