let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for ASeq being SetSequence of
for P being Probability of Sigma holds
( P * (@Partial_Union ASeq) is convergent & lim (P * (@Partial_Union ASeq)) = sup (P * (@Partial_Union ASeq)) & lim (P * (@Partial_Union ASeq)) = P . (Union ASeq) )
let Sigma be SigmaField of Omega; :: thesis: for ASeq being SetSequence of
for P being Probability of Sigma holds
( P * (@Partial_Union ASeq) is convergent & lim (P * (@Partial_Union ASeq)) = sup (P * (@Partial_Union ASeq)) & lim (P * (@Partial_Union ASeq)) = P . (Union ASeq) )
let ASeq be SetSequence of ; :: thesis: for P being Probability of Sigma holds
( P * (@Partial_Union ASeq) is convergent & lim (P * (@Partial_Union ASeq)) = sup (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)) = sup (P * (@Partial_Union ASeq)) & lim (P * (@Partial_Union ASeq)) = P . (Union ASeq) )
A1: @Partial_Union ASeq is non-descending by Th13;
then P * (@Partial_Union ASeq) is convergent by PROB_2:20;
then P * (@Partial_Union ASeq) is bounded by SEQ_2:27;
then A2: P * (@Partial_Union ASeq) is bounded_above ;
A3: P * (@Partial_Union ASeq) is non-decreasing by Th42;
lim (P * (@Partial_Union ASeq)) = P . (Union (@Partial_Union ASeq)) by A1, PROB_2:20
.= P . (Union ASeq) by Th17 ;
hence ( P * (@Partial_Union ASeq) is convergent & lim (P * (@Partial_Union ASeq)) = sup (P * (@Partial_Union ASeq)) & lim (P * (@Partial_Union ASeq)) = P . (Union ASeq) ) by A1, A2, A3, PROB_2:20, RINFSUP1:24; :: thesis: verum