let Omega be 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 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 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 Nat holds BSeq . n = (ASeq . n) /\ B

let B be Event of Sigma; :: thesis: ex BSeq being SetSequence of Sigma st

for n being Nat holds BSeq . n = (ASeq . n) /\ B

deffunc H_{1}( 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_{1}(n) ) )
from FUNCT_1:sch 4();

f . x in bool Omega ;

then reconsider f = f as SetSequence of Omega by A1, FUNCT_2:3;

then reconsider f = f as SetSequence of Sigma by RELAT_1:def 19;

take f ; :: thesis: for n being Nat holds f . n = (ASeq . n) /\ B

let n be Nat; :: thesis: f . n = (ASeq . n) /\ B

reconsider n = n as Element of NAT by ORDINAL1:def 12;

f . n = H_{1}(n)
by A1;

hence f . n = (ASeq . n) /\ B ; :: thesis: verum

for ASeq being SetSequence of Sigma

for B being Event of Sigma ex BSeq being SetSequence of Sigma st

for n being 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 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 Nat holds BSeq . n = (ASeq . n) /\ B

let B be Event of Sigma; :: thesis: ex BSeq being SetSequence of Sigma st

for n being Nat holds BSeq . n = (ASeq . n) /\ B

deffunc H

consider f being Function such that

A1: ( dom f = NAT & ( for n being Element of NAT holds f . n = H

now :: thesis: for m being Nat holds f . m in bool Omega

then
for x being object st x in NAT holds let m be Nat; :: thesis: f . m in bool Omega

reconsider mm = m as Element of NAT by ORDINAL1:def 12;

(ASeq . m) /\ B in bool Omega ;

then f . mm in bool Omega by A1;

hence f . m in bool Omega ; :: thesis: verum

end;reconsider mm = m as Element of NAT by ORDINAL1:def 12;

(ASeq . m) /\ B in bool Omega ;

then f . mm in bool Omega by A1;

hence f . m in bool Omega ; :: thesis: verum

f . x in bool Omega ;

then reconsider f = f as SetSequence of Omega by A1, FUNCT_2:3;

now :: thesis: for m being Nat holds f . m in Sigma

then
rng f c= Sigma
by NAT_1:52;let m be Nat; :: thesis: f . m in Sigma

reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

(ASeq . m1) /\ B in Sigma ;

hence f . m in Sigma by A1; :: thesis: verum

end;reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

(ASeq . m1) /\ B in Sigma ;

hence f . m in Sigma by A1; :: thesis: verum

then reconsider f = f as SetSequence of Sigma by RELAT_1:def 19;

take f ; :: thesis: for n being Nat holds f . n = (ASeq . n) /\ B

let n be Nat; :: thesis: f . n = (ASeq . n) /\ B

reconsider n = n as Element of NAT by ORDINAL1:def 12;

f . n = H

hence f . n = (ASeq . n) /\ B ; :: thesis: verum