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 ;
then A3: P * (Complement ASeq) is convergent by PROB_1:def 8;
A4: now :: thesis: for n being Nat holds (P * ASeq) . n = 1 - ((P * (Complement ASeq)) . n)
let n be Nat; :: thesis: (P * ASeq) . n = 1 - ((P * (Complement ASeq)) . n)
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
(P * (Complement ASeq)) . n = P . ((Complement ASeq) . nn) 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) . nn) 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 ; :: 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, Th2
.= 1 - (1 - (P . V)) by
.= P . (Union ASeq) ; :: thesis: verum