for Omega, I being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for a being Element of Sigma
for F being ManySortedSigmaField of I,Sigma st F is_independent_wrt P & a in tailSigmaField (F,I) & not P . a = 0 holds
P . a = 1