let X be set ; :: thesis: for A1 being SetSequence of X
for Si being SigmaField of X holds
( A1 is SetSequence of Si iff for n being Nat holds A1 . n is Event of Si )
let A1 be SetSequence of X; :: thesis: for Si being SigmaField of X holds
( A1 is SetSequence of Si iff for n being Nat holds A1 . n is Event of Si )
let Si be SigmaField of X; :: thesis: ( A1 is SetSequence of Si iff for n being Nat holds A1 . n is Event of Si )
thus ( A1 is SetSequence of Si implies for n being Nat holds A1 . n is Event of Si ) :: thesis: ( ( for n being Nat holds A1 . n is Event of Si ) implies A1 is SetSequence of Si )

proof

assume A1 is SetSequence of Si ; :: thesis: for n being Nat holds A1 . n is Event of Si
then A1: rng A1 c= Si by RELAT_1:def 19;
for n being Nat holds A1 . n is Event of Si by NAT_1:51, A1;
hence for n being Nat holds A1 . n is Event of Si ; :: thesis: verum

end;

assume A2: for n being Nat holds A1 . n is Event of Si ; :: thesis: A1 is SetSequence of Si
for n being Nat holds A1 . n in Si

proof

let n be Nat; :: thesis: A1 . n in Si
A1 . n is Event of Si by A2;
hence A1 . n in Si ; :: thesis: verum

end;

then rng A1 c= Si by NAT_1:52;
hence A1 is SetSequence of Si by RELAT_1:def 19; :: thesis: verum