theorem Th14: :: KOLMOG01:14

for Omega, I being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being ManySortedSigmaField of I,Sigma
for J, K being non empty Subset of I st F is_independent_wrt P & J misses K holds
for u, v being Event of Sigma st u in sigUn (F,J) & v in sigUn (F,K) holds
P . (u /\ v) = (P . u) * (P . v)