let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being Function of NAT ,(COM Sigma,P)
for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for F being Function of NAT ,(COM Sigma,P)
for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
let P be Probability of Sigma; :: thesis: for F being Function of NAT ,(COM Sigma,P)
for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
let F be Function of NAT ,(COM Sigma,P); :: thesis: for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n)
let G be SetSequence of Sigma; :: thesis: ex CSeq being SetSequence of Omega st
for n being Element of NAT holds CSeq . n = (F . n) \ (G . n)
defpred S₁[ 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 Element of bool Omega st S₁[t,A]

proof

let t be Element of NAT ; :: thesis: ex A being Element of bool Omega st S₁[t,A]
F . t is Element of COM Sigma,P ;
then reconsider A = (F . t) \ (G . t) as Element of bool Omega by XBOOLE_1:1;
take A ; :: thesis: S₁[t,A]
thus S₁[t,A] ; :: thesis: verum

end;

ex H being Function of NAT ,(bool Omega) st
for t being Element of NAT holds S₁[t,H . t] from FUNCT_2:sch 3(A1);
then consider H being Function of NAT ,(bool Omega) 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