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 ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for F being Function of NAT , COM Sigma,P ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
let P be Probability of Sigma; :: thesis: for F being Function of NAT , COM Sigma,P ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . n)
let F be Function of NAT , COM Sigma,P; :: thesis: ex BSeq being SetSequence of Sigma st
for n being Element of NAT holds BSeq . n in ProbPart (F . 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 in ProbPart (F . n);
A1: for t being Element of NAT ex A being Element of Sigma st S₁[t,A]

proof

let t be Element of NAT ; :: thesis: ex A being Element of Sigma st S₁[t,A]
consider A being Element of ProbPart (F . t);
reconsider A = A as Element of Sigma by Def7;
take A ; :: thesis: S₁[t,A]
thus S₁[t,A] ; :: thesis: verum

end;

ex G being Function of NAT ,Sigma st
for t being Element of NAT holds S₁[t,G . t] from FUNCT_2:sch 3(A1);
then consider G being Function of NAT ,Sigma such that
A2: for t, n being Element of NAT
for y being set st n = t & y = G . t holds
y in ProbPart (F . n) ;
for n being Nat holds G . n in Sigma

proof

let n be Nat; :: thesis: G . n in Sigma
reconsider n = n as Element of NAT by ORDINAL1:def 13;
G . n in Sigma ;
hence G . n in Sigma ; :: thesis: verum

end;

then A3: rng G c= Sigma by NAT_1:53;
reconsider BSeq = G as SetSequence of Omega by FUNCT_2:9;
reconsider BSeq = BSeq as SetSequence of Sigma by A3, PROB_1:def 9;
take BSeq ; :: thesis: for n being Element of NAT holds BSeq . n in ProbPart (F . n)
thus for n being Element of NAT holds BSeq . n in ProbPart (F . n) by A2; :: thesis: verum