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 8;

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:15
.= P . ((ASeq . n) `) by PROB_1:def 2
.= P . (([#] Sigma) \ (ASeq . n))
.= 1 - (P . (ASeq . n)) by PROB_1:32
.= 1 - ((P * ASeq) . n) by FUNCT_2:15
.= 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:26;
Intersection (Complement ASeq) = ([#] Sigma) \ (Union ASeq) ;
then A5: P . (Intersection (Complement ASeq)) = 1 - (P . V) by PROB_1:32;
thus lim (P * ASeq) = 1 - (lim (P * (Complement ASeq))) by A3, A4, Th5
.= 1 - (1 - (P . V)) by A2, A5, PROB_1:def 8
.= P . (Union ASeq) ; :: thesis: verum