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

( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union 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

( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

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

( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

let P be Probability of Sigma; :: thesis: ( ASeq is V77() implies ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) ) )

assume ASeq is V77() ; :: thesis: ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

then P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by Th44;

hence ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) ) by Th41; :: thesis: verum

for ASeq being SetSequence of Sigma

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

( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union 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

( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

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

( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

let P be Probability of Sigma; :: thesis: ( ASeq is V77() implies ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) ) )

assume ASeq is V77() ; :: thesis: ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

then P * (Partial_Union ASeq) = Partial_Sums (P * ASeq) by Th44;

hence ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) ) by Th41; :: thesis: verum