theorem Th4: :: KOLMOG01:4

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B being non empty Subset of Sigma
for b being Element of B
for f being SetSequence of Sigma st ( for n being Element of NAT
for b being Element of B holds P . ((f . n) /\ b) = (P . (f . n)) * (P . b) ) & f is disjoint_valued holds
P . (b /\ (Union f)) = (P . b) * (P . (Union f))