let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being sequence of (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 sequence of (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 sequence of (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 sequence of (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]
set A = the Element of ProbPart (F . t);
reconsider A = the Element of ProbPart (F . t) as Element of Sigma by Def7;
take A ; :: thesis: S₁[t,A]
thus S₁[t,A] ; :: thesis: verum

end;

ex G being sequence of Sigma st
for t being Element of NAT holds S₁[t,G . t] from FUNCT_2:sch 3(A1);
then consider G being sequence of 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) ;
reconsider BSeq = G as SetSequence of Omega by FUNCT_2:7;
reconsider BSeq = BSeq as SetSequence of Sigma ;
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