let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

P . (Union ASeq) = Sum (P * ASeq)

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

P . (Union ASeq) = Sum (P * ASeq)

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma st ASeq is V77() holds

P . (Union ASeq) = Sum (P * ASeq)

let P be Probability of Sigma; :: thesis: ( ASeq is V77() implies P . (Union ASeq) = Sum (P * ASeq) )

assume ASeq is V77() ; :: thesis: P . (Union ASeq) = Sum (P * ASeq)

then lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) by Th45;

hence P . (Union ASeq) = Sum (P * ASeq) by SERIES_1:def 3; :: thesis: verum

for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

P . (Union ASeq) = Sum (P * ASeq)

let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of Sigma

for P being Probability of Sigma st ASeq is V77() holds

P . (Union ASeq) = Sum (P * ASeq)

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma st ASeq is V77() holds

P . (Union ASeq) = Sum (P * ASeq)

let P be Probability of Sigma; :: thesis: ( ASeq is V77() implies P . (Union ASeq) = Sum (P * ASeq) )

assume ASeq is V77() ; :: thesis: P . (Union ASeq) = Sum (P * ASeq)

then lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) by Th45;

hence P . (Union ASeq) = Sum (P * ASeq) by SERIES_1:def 3; :: thesis: verum