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 )

for n being Nat holds A1 . n in Si

hence A1 is SetSequence of Si by RELAT_1:def 19; :: thesis: verum

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 A2:
for n being Nat holds A1 . n is Event of Si
; :: thesis: A1 is SetSequence of Si
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;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

for n being Nat holds A1 . n in Si

proof

then
rng A1 c= Si
by NAT_1:52;
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;A1 . n is Event of Si by A2;

hence A1 . n in Si ; :: thesis: verum

hence A1 is SetSequence of Si by RELAT_1:def 19; :: thesis: verum