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))
for G being sequence of S ex H being sequence of (bool X) st
for n being Element of NAT holds H . n = (F . n) \ (G . n)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for F being sequence of (COM (S,M))
for G being sequence of S ex H being sequence of (bool X) st
for n being Element of NAT holds H . n = (F . n) \ (G . n)

let M be sigma_Measure of S; :: thesis: for F being sequence of (COM (S,M))
for G being sequence of S ex H being sequence of (bool X) st
for n being Element of NAT holds H . n = (F . n) \ (G . n)

let F be sequence of (COM (S,M)); :: thesis: for G being sequence of S ex H being sequence of (bool X) st
for n being Element of NAT holds H . n = (F . n) \ (G . n)

let G be sequence of S; :: thesis: ex H being sequence of (bool X) st
for n being Element of NAT holds H . n = (F . n) \ (G . 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 = (F . n) \ (G . n);
A1: for t being Element of NAT ex A being Subset of X st S1[t,A]
proof
let t be Element of NAT ; :: thesis: ex A being Subset of X st S1[t,A]
F . t is Element of COM (S,M) ;
then reconsider A = (F . t) \ (G . t) as Subset of X by XBOOLE_1:1;
take A ; :: thesis: S1[t,A]
thus S1[t,A] ; :: thesis: verum
end;
ex H being sequence of (bool X) st
for t being Element of NAT holds S1[t,H . t] from then consider H being sequence of (bool X) such that
A2: for t, n being Element of NAT
for y being set st n = t & y = H . t holds
y = (F . n) \ (G . n) ;
take H ; :: thesis: for n being Element of NAT holds H . n = (F . n) \ (G . n)
thus for n being Element of NAT holds H . n = (F . n) \ (G . n) by A2; :: thesis: verum