let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds
ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds
ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
let P be Probability of Sigma; :: thesis: for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds
ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
let BSeq be SetSequence of Omega; :: thesis: ( ( for n being Element of NAT holds BSeq . n is thin of P ) implies ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) )
defpred S₁[ Element of NAT , set ] means for n being Element of NAT
for y being set st n = $1 & y = $2 holds
( y in Sigma & BSeq . n c= y & P . y = 0 );
assume A1: for n being Element of NAT holds BSeq . n is thin of P ; :: thesis: ex CSeq being SetSequence of Sigma st
for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
A2: for t being Element of NAT ex A being Element of Sigma st S₁[t,A]

proof

let t be Element of NAT ; :: thesis: ex A being Element of Sigma st S₁[t,A]
BSeq . t is thin of P by A1;
then consider A being set such that
A3: A in Sigma and
A4: ( BSeq . t c= A & P . A = 0 ) by Def4;
reconsider A = A as Element of Sigma by A3;
take A ; :: thesis: S₁[t,A]
thus S₁[t,A] by A4; :: thesis: verum

end;

ex G being sequence of Sigma st
for t being Element of NAT holds S₁[t,G . t] from FUNCT_2:sch 3(A2);
then consider G being sequence of Sigma such that
A5: for t, n being Element of NAT
for y being set st n = t & y = G . t holds
( y in Sigma & BSeq . n c= y & P . y = 0 ) ;
reconsider CSeq = G as SetSequence of Omega by FUNCT_2:7;
reconsider CSeq = CSeq as SetSequence of Sigma ;
take CSeq ; :: thesis: for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )
thus for n being Element of NAT holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) by A5; :: thesis: verum