let X be set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for F being sequence of (COM (S,M)) ex G being sequence of S st

for n being Element of NAT holds G . n in MeasPart (F . n)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being sequence of (COM (S,M)) ex G being sequence of S st

for n being Element of NAT holds G . n in MeasPart (F . n)

let M be sigma_Measure of S; :: thesis: for F being sequence of (COM (S,M)) ex G being sequence of S st

for n being Element of NAT holds G . n in MeasPart (F . n)

let F be sequence of (COM (S,M)); :: thesis: ex G being sequence of S st

for n being Element of NAT holds G . n in MeasPart (F . n)

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 MeasPart (F . n);

A1: 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(A1);

then consider G being sequence of S such that

A2: for t, n being Element of NAT

for y being set st n = t & y = G . t holds

y in MeasPart (F . n) ;

take G ; :: thesis: for n being Element of NAT holds G . n in MeasPart (F . n)

thus for n being Element of NAT holds G . n in MeasPart (F . n) by A2; :: thesis: verum

for M being sigma_Measure of S

for F being sequence of (COM (S,M)) ex G being sequence of S st

for n being Element of NAT holds G . n in MeasPart (F . n)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being sequence of (COM (S,M)) ex G being sequence of S st

for n being Element of NAT holds G . n in MeasPart (F . n)

let M be sigma_Measure of S; :: thesis: for F being sequence of (COM (S,M)) ex G being sequence of S st

for n being Element of NAT holds G . n in MeasPart (F . n)

let F be sequence of (COM (S,M)); :: thesis: ex G being sequence of S st

for n being Element of NAT holds G . n in MeasPart (F . n)

defpred S

for y being set st n = $1 & y = $2 holds

y in MeasPart (F . n);

A1: 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]

set A = the Element of MeasPart (F . t);

reconsider A = the Element of MeasPart (F . t) as Element of S by Def4;

take A ; :: thesis: S_{1}[t,A]

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

end;set A = the Element of MeasPart (F . t);

reconsider A = the Element of MeasPart (F . t) as Element of S by Def4;

take A ; :: thesis: S

thus S

for t being Element of NAT holds S

then consider G being sequence of S such that

A2: for t, n being Element of NAT

for y being set st n = t & y = G . t holds

y in MeasPart (F . n) ;

take G ; :: thesis: for n being Element of NAT holds G . n in MeasPart (F . n)

thus for n being Element of NAT holds G . n in MeasPart (F . n) by A2; :: thesis: verum