for n being Nat
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 V77() holds
(P * (Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n