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;

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 A2, A5, PROB_1:def 8

.= P . (Union ASeq) ; :: thesis: verum

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 :: thesis: for n being Nat holds (P * ASeq) . n = 1 - ((P * (Complement ASeq)) . n)

hence
P * ASeq is convergent
by A3, Th2; :: thesis: lim (P * ASeq) = P . (Union ASeq)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;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

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 A2, A5, PROB_1:def 8

.= P . (Union ASeq) ; :: thesis: verum