let Omega be non empty finite set ; :: thesis: for f being Function of Omega,REAL
for P being Function of (bool Omega),REAL st ( for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) holds
P is Probability of Trivial-SigmaField Omega
let f be Function of Omega,REAL; :: thesis: for P being Function of (bool Omega),REAL st ( for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) holds
P is Probability of Trivial-SigmaField Omega
let P be Function of (bool Omega),REAL; :: thesis: ( ( for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) ) & P . Omega = 1 & ( for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ) implies P is Probability of Trivial-SigmaField Omega )
assume that
A1: for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) and
A2: P . Omega = 1 and
A3: for z being finite Subset of Omega holds P . z = setopfunc (z,Omega,REAL,f,addreal) ; :: thesis: P is Probability of Trivial-SigmaField Omega
A4: for A, B being Event of Trivial-SigmaField Omega st A misses B holds
P . (A \/ B) = (P . A) + (P . B)

proof

let A, B be Event of Trivial-SigmaField Omega; :: thesis: ( A misses B implies P . (A \/ B) = (P . A) + (P . B) )
assume A5: A misses B ; :: thesis: P . (A \/ B) = (P . A) + (P . B)
reconsider A0 = A, B0 = B as finite Subset of Omega ;
A6: Omega = dom f by FUNCT_2:def 1;
thus P . (A \/ B) = setopfunc ((A0 \/ B0),Omega,REAL,f,addreal) by A3
.= addreal . ((setopfunc (A0,Omega,REAL,f,addreal)),(setopfunc (B0,Omega,REAL,f,addreal))) by A5, A6, BHSP_5:14
.= addreal . ((setopfunc (A0,Omega,REAL,f,addreal)),(P . B)) by A3
.= addreal . ((P . A),(P . B)) by A3
.= (P . A) + (P . B) by BINOP_2:def 9 ; :: thesis: verum

end;

A7: for A being Event of Trivial-SigmaField Omega holds 0 <= P . A by A1;
for ASeq being SetSequence of Trivial-SigmaField Omega st ASeq is non-ascending holds
( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )

proof

let ASeq be SetSequence of Trivial-SigmaField Omega; :: thesis: ( ASeq is non-ascending implies ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) )
assume ASeq is non-ascending ; :: thesis: ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) )
then consider N being Nat such that
A8: for m being Nat st N <= m holds
Intersection ASeq = ASeq . m by RANDOM_1:15;

now :: thesis: for m being Nat st N <= m holds
(P * ASeq) . m = P . (Intersection ASeq)

let m be Nat; :: thesis: ( N <= m implies (P * ASeq) . m = P . (Intersection ASeq) )
assume A9: N <= m ; :: thesis: (P * ASeq) . m = P . (Intersection ASeq)
m in NAT by ORDINAL1:def 12;
then m in dom ASeq by FUNCT_2:def 1;
hence (P * ASeq) . m = P . (ASeq . m) by FUNCT_1:13
.= P . (Intersection ASeq) by A8, A9 ;
:: thesis: verum

end;

hence ( P * ASeq is convergent & lim (P * ASeq) = P . (Intersection ASeq) ) by PROB_1:1; :: thesis: verum

end;

hence P is Probability of Trivial-SigmaField Omega by A7, A4, A2, PROB_1:def 8; :: thesis: verum