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
AS1: for x being set st x c= Omega holds
( 0 <= P . x & P . x <= 1 ) and
AS2: P . Omega = 1 and
AS3: for z being finite Subset of Omega holds P . z = setopfunc z,Omega,REAL ,f,addreal ; :: thesis: P is Probability of Trivial-SigmaField Omega
A2: 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 A3: A misses B ; :: thesis: P . (A \/ B) = (P . A) + (P . B)
reconsider A0 = A, B0 = B as finite Subset of Omega ;
A31: Omega = dom f by FUNCT_2:def 1;
thus P . (A \/ B) = setopfunc (A0 \/ B0),Omega,REAL ,f,addreal by AS3
.= addreal . (setopfunc A0,Omega,REAL ,f,addreal ),(setopfunc B0,Omega,REAL ,f,addreal ) by A3, A31, BHSP_5:14
.= addreal . (setopfunc A0,Omega,REAL ,f,addreal ),(P . B) by AS3
.= addreal . (P . A),(P . B) by AS3
.= (P . A) + (P . B) by BINOP_2:def 9 ; :: thesis: verum

end;

A4: for A being Event of Trivial-SigmaField Omega holds 0 <= P . A by AS1;
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 Element of NAT such that
A6: for m being Element of NAT st N <= m holds
Intersection ASeq = ASeq . m by RANDOM_1:15;

now

let m be Element of NAT ; :: thesis: ( N <= m implies (P * ASeq) . m = P . (Intersection ASeq) )
assume A7: N <= m ; :: thesis: (P * ASeq) . m = P . (Intersection ASeq)
m in NAT ;
then m in dom ASeq by FUNCT_2:def 1;
hence (P * ASeq) . m = P . (ASeq . m) by FUNCT_1:23
.= P . (Intersection ASeq) by A6, A7 ;
:: thesis: verum

end;

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

end;

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