theorem Th44: :: PROB_3:44

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is disjoint_valued holds
P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by Th43;