theorem Th32: :: PROB_4:32

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being sequence of (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)