let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Function of Sigma,REAL holds
( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( 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 Function of Sigma,REAL holds
( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( 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 Function of Sigma,REAL; :: thesis: ( P is Probability of Sigma iff ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) )
thus ( P is Probability of Sigma implies ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) ) ) by Lm2, PROB_1:def 8; :: thesis: ( ( for A being Event of Sigma holds 0 <= P . A ) & P . Omega = 1 & ( for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) ) & ( for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ) implies P is Probability of Sigma )
assume that
A1: for A being Event of Sigma holds 0 <= P . A and
A2: P . Omega = 1 and
A3: for A, B being Event of Sigma st A misses B holds
P . (A \/ B) = (P . A) + (P . B) and
A4: for ASeq being SetSequence of Sigma st ASeq is non-descending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Union ASeq) ) ; :: thesis: P is Probability of Sigma
for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

proof

let ASeq be SetSequence of Sigma; :: thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )
assume A5: ASeq is non-ascending ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
Intersection ASeq = @Intersection ASeq ;
then reconsider V = Intersection ASeq as Event of Sigma ;
set BSeq = Complement ASeq;
A6: for A being Event of Sigma holds P . (A `) = 1 - (P . A)

proof

let A be Event of Sigma; :: thesis: P . (A `) = 1 - (P . A)
reconsider B = A ` as Event of Sigma by PROB_1:20;
A7: A misses B by SUBSET_1:24;
1 = P . ([#] Omega) by A2
.= P . (A \/ B) by SUBSET_1:10
.= (P . A) + (P . B) by A3, A7 ;
hence P . (A `) = 1 - (P . A) ; :: thesis: verum

end;

A8: 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
.= 1 - (P . (ASeq . n)) by A6
.= 1 - ((P * ASeq) . nn) by FUNCT_2:15
.= 1 + (- ((P * ASeq) . n)) ;
hence (P * ASeq) . n = 1 - ((P * (Complement ASeq)) . n) ; :: thesis: verum

end;

Union (Complement ASeq) = (Intersection ASeq) ` ;
then A9: P . (Union (Complement ASeq)) = 1 - (P . V) by A6;
A10: Complement ASeq is non-descending by A5, Th8;
then A11: P * (Complement ASeq) is convergent by A4;
hence P * ASeq is convergent by A8, Th2; :: thesis: lim (P * ASeq) = P . (Intersection ASeq)
thus lim (P * ASeq) = 1 - (lim (P * (Complement ASeq))) by A11, A8, Th2
.= 1 - (1 - (P . V)) by A4, A10, A9
.= P . (Intersection ASeq) ; :: thesis: verum

end;

hence P is Probability of Sigma by A1, A2, A3, PROB_1:def 8; :: thesis: verum