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) )

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

hence
P is Probability of Sigma
by A1, A2, A3, PROB_1:def 8; :: thesis: verum
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)

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

A8: now :: thesis: for n being Nat holds (P * ASeq) . n = 1 - ((P * (Complement ASeq)) . n)

Union (Complement ASeq) = (Intersection 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

.= 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;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

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