let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for B being Event of Sigma ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B
let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma
for B being Event of Sigma ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B
let ASeq be SetSequence of Sigma; :: thesis: for B being Event of Sigma ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B
let B be Event of Sigma; :: thesis: ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B
deffunc H₁( Element of NAT ) -> Event of Sigma = (ASeq . $1) /\ B;
consider f being Function such that
A1: ( dom f = NAT & ( for n being Element of NAT holds f . n = H₁(n) ) ) from FUNCT_1:sch 4();

now

let m be Element of NAT ; :: thesis: f . m in bool Omega
(ASeq . m) /\ B in bool Omega ;
hence f . m in bool Omega by A1; :: thesis: verum

end;

then for x being set st x in NAT holds
f . x in bool Omega ;
then reconsider f = f as SetSequence of Omega by A1, FUNCT_2:5;

now

let m be Nat; :: thesis: f . m in Sigma
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
(ASeq . m1) /\ B in Sigma ;
hence f . m in Sigma by A1; :: thesis: verum

end;

then rng f c= Sigma by NAT_1:53;
then reconsider f = f as SetSequence of Sigma by RELAT_1:def 19;
take f ; :: thesis: for n being Element of NAT holds f . n = (ASeq . n) /\ B
thus for n being Element of NAT holds f . n = (ASeq . n) /\ B by A1; :: thesis: verum