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_{1}[ 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_{1}[t,A]

for t being Element of NAT holds S_{1}[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

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

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

proof

ex G being sequence of S st
let t be Element of NAT ; :: thesis: ex A being Element of S st S_{1}[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_{1}[t,A]

thus S_{1}[t,A]
by A4; :: thesis: verum

end;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

thus S

for t being Element of NAT holds S

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