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 S1[ 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 S1[t,A]
proof
let t be Element of NAT ; :: thesis: ex A being Element of S st S1[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: S1[t,A]
thus S1[t,A] ; :: thesis: verum
end;
ex G being sequence of S st
for t being Element of NAT holds S1[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