let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of (bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds
ex G being sequence of S st
for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being sequence of (bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds
ex G being sequence of S st
for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. )
let M be sigma_Measure of S; :: thesis: for F being sequence of (bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds
ex G being sequence of S st
for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. )
let F be sequence of (bool X); :: thesis: ( ( for n being Element of NAT holds F . n is thin of M ) implies ex G being sequence of S st
for n being Element of NAT holds
( F . n c= G . n & M . (G . 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 S & F . n c= y & M . y = 0. );
assume A1: for n being Element of NAT holds F . n is thin of M ; :: thesis: ex G being sequence of S st
for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. )
A2: for t being Element of NAT ex A being Element of S st S₁[t,A]

proof

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

end;

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