theorem Th41: :: PROB_3:41

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( P * (Partial_Union ASeq) is convergent & lim (P * (Partial_Union ASeq)) = upper_bound (P * (Partial_Union ASeq)) & lim (P * (Partial_Union ASeq)) = P . (Union ASeq) )