let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )
let P be Probability of Sigma; :: thesis: for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )
let ASeq be SetSequence of Sigma; :: thesis: ( ASeq is non-descending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) )
assume A1: ASeq is non-descending ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) )
set BSeq = @Complement ASeq;
A2: @Complement ASeq is non-ascending by A1, Lm1;
then A3: P * (@Complement ASeq) is convergent by PROB_1:def 13;

A4: now

let n be Element of NAT ; :: thesis: (P * ASeq) . n = 1 - ((P * (@Complement ASeq)) . n)
(P * (@Complement ASeq)) . n = P . ((@Complement ASeq) . n) by FUNCT_2:21
.= P . ((ASeq . n) ` ) by PROB_1:def 4
.= P . (([#] Sigma) \ (ASeq . n))
.= 1 - (P . (ASeq . n)) by PROB_1:68
.= 1 - ((P * ASeq) . n) by FUNCT_2:21
.= 1 + (- ((P * ASeq) . n)) ;
hence (P * ASeq) . n = 1 - ((P * (@Complement ASeq)) . n) ; :: thesis: verum

end;

hence P * ASeq is convergent by A3, Th5; :: thesis: lim (P * ASeq) = P . (Union ASeq)
reconsider V = Union ASeq as Event of Sigma by PROB_1:58;
Intersection (@Complement ASeq) = ([#] Sigma) \ (Union ASeq) ;
then A5: P . (Intersection (@Complement ASeq)) = 1 - (P . V) by PROB_1:68;
thus lim (P * ASeq) = 1 - (lim (P * (@Complement ASeq))) by A3, A4, Th5
.= 1 - (1 - (P . V)) by A2, A5, PROB_1:def 13
.= P . (Union ASeq) ; :: thesis: verum