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 holds

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

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

for P being Probability of Sigma holds

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

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds

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

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

A1: P * (Partial_Union ASeq) is non-decreasing by Th37;

A2: Partial_Union ASeq is V75() by Th11;

then P * (Partial_Union ASeq) is convergent by PROB_2:10;

then A3: P * (Partial_Union ASeq) is bounded ;

lim (P * (Partial_Union ASeq)) = P . (Union (Partial_Union ASeq)) by A2, PROB_2:10

.= P . (Union ASeq) by Th15 ;

hence ( P * (Partial_Union ASeq) is convergent & lim (P * (Partial_Union ASeq)) = upper_bound (P * (Partial_Union ASeq)) & lim (P * (Partial_Union ASeq)) = P . (Union ASeq) ) by A2, A3, A1, PROB_2:10, RINFSUP1:24; :: thesis: verum

for ASeq being SetSequence of Sigma

for P being Probability of Sigma holds

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

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

for P being Probability of Sigma holds

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

let ASeq be SetSequence of Sigma; :: thesis: for P being Probability of Sigma holds

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

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

A1: P * (Partial_Union ASeq) is non-decreasing by Th37;

A2: Partial_Union ASeq is V75() by Th11;

then P * (Partial_Union ASeq) is convergent by PROB_2:10;

then A3: P * (Partial_Union ASeq) is bounded ;

lim (P * (Partial_Union ASeq)) = P . (Union (Partial_Union ASeq)) by A2, PROB_2:10

.= P . (Union ASeq) by Th15 ;

hence ( P * (Partial_Union ASeq) is convergent & lim (P * (Partial_Union ASeq)) = upper_bound (P * (Partial_Union ASeq)) & lim (P * (Partial_Union ASeq)) = P . (Union ASeq) ) by A2, A3, A1, PROB_2:10, RINFSUP1:24; :: thesis: verum