theorem Th64: :: PROB_3:64

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma
for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds
ASeq . k = FSeq . k ) & ( for k being Nat st not k in dom FSeq holds
ASeq . k = {} ) holds
( Partial_Sums (P * ASeq) is convergent & Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) & P . (Union ASeq) <= Sum (P * ASeq) & Sum (P * FSeq) = Sum (P * ASeq) )