let Omega be non empty set ; :: thesis: for ASeq being SetSequence of Omega
for Sigma being SigmaField of Omega holds
( ASeq is SetSequence of Sigma iff for n being Element of NAT holds ASeq . n is Event of Sigma )
let ASeq be SetSequence of Omega; :: thesis: for Sigma being SigmaField of Omega holds
( ASeq is SetSequence of Sigma iff for n being Element of NAT holds ASeq . n is Event of Sigma )
let Sigma be SigmaField of Omega; :: thesis: ( ASeq is SetSequence of Sigma iff for n being Element of NAT holds ASeq . n is Event of Sigma )
thus ( ASeq is SetSequence of Sigma implies for n being Element of NAT holds ASeq . n is Event of Sigma ) :: thesis: ( ( for n being Element of NAT holds ASeq . n is Event of Sigma ) implies ASeq is SetSequence of Sigma )

proof

assume ASeq is SetSequence of Sigma ; :: thesis: for n being Element of NAT holds ASeq . n is Event of Sigma
then A1: rng ASeq c= Sigma by RELAT_1:def 19;
for n being Element of NAT holds ASeq . n is Event of Sigma

proof

let n be Element of NAT ; :: thesis: ASeq . n is Event of Sigma
ASeq . n in rng ASeq by NAT_1:52;
hence ASeq . n is Event of Sigma by A1; :: thesis: verum

end;

hence for n being Element of NAT holds ASeq . n is Event of Sigma ; :: thesis: verum

end;

assume A2: for n being Element of NAT holds ASeq . n is Event of Sigma ; :: thesis: ASeq is SetSequence of Sigma
for n being Nat holds ASeq . n in Sigma

proof

let n be Nat; :: thesis: ASeq . n in Sigma
n in NAT by ORDINAL1:def 13;
then ASeq . n is Event of Sigma by A2;
hence ASeq . n in Sigma ; :: thesis: verum

end;

then rng ASeq c= Sigma by NAT_1:53;
hence ASeq is SetSequence of Sigma by RELAT_1:def 19; :: thesis: verum