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 disjoint_valued 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 disjoint_valued 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 disjoint_valued 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 disjoint_valued 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 disjoint_valued ; :: 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