let Omega be non empty finite set ; 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; 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; ( ( 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)
; 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;
( A misses B implies P . (A \/ B) = (P . A) + (P . B) )
assume A5:
A misses B
;
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
;
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) )
hence
P is Probability of Trivial-SigmaField Omega
by A7, A4, A2, PROB_1:def 8; verum