reconsider C = {} as thin of P by Th24;
defpred S1[ object , object ] means for x, y being set st x in COM (Sigma,P) & x = $1 & y = $2 holds
for B being set st B in Sigma holds
for C being thin of P st x = B \/ C holds
y = P . B;
set B = {} ;
A1:
{} is thin of P
by Th24;
A2:
for x being object st x in COM (Sigma,P) holds
ex y being object st
( y in REAL & S1[x,y] )
consider comP being Function of (COM (Sigma,P)),REAL such that
A4:
for x being object st x in COM (Sigma,P) holds
S1[x,comP . x]
from FUNCT_2:sch 1(A2);
A5:
for B being set st B in Sigma holds
for C being thin of P holds comP . (B \/ C) = P . B
A7:
for BSeq being SetSequence of COM (Sigma,P) st BSeq is V126() holds
Sum (comP * BSeq) = comP . (Union BSeq)
A48:
for x being Element of COM (Sigma,P) holds comP . x >= 0
{} = {} \/ C
;
then A51: comP . {} =
P . {}
by A5, PROB_1:4
.=
0
by VALUED_0:def 19
;
A52:
for A, B being Event of COM (Sigma,P) st A misses B holds
comP . (A \/ B) = (comP . A) + (comP . B)
proof
let A,
B be
Event of
COM (
Sigma,
P);
( A misses B implies comP . (A \/ B) = (comP . A) + (comP . B) )
assume A53:
A misses B
;
comP . (A \/ B) = (comP . A) + (comP . B)
reconsider A1 =
A,
B1 =
B as
Subset of
Omega ;
reconsider BSeq = (
A1,
B1)
followed_by ({} Omega) as
SetSequence of
Omega ;
A54:
BSeq . 1
= B
by FUNCT_7:123;
A55:
BSeq . 0 = A
by FUNCT_7:122;
for
n being
Nat holds
BSeq . n in COM (
Sigma,
P)
then
rng BSeq c= COM (
Sigma,
P)
by NAT_1:52;
then reconsider BSeq =
BSeq as
SetSequence of
COM (
Sigma,
P)
by RELAT_1:def 19;
for
m being
Nat st 2
<= m holds
(Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B)
then A65:
(
Union BSeq = A \/ B &
Sum (comP * BSeq) = (comP . A) + (comP . B) )
by DYNKIN:3, PROB_1:1;
BSeq is
V126()
by A53, Th3;
hence
comP . (A \/ B) = (comP . A) + (comP . B)
by A7, A65;
verum
end;
A66:
for A, B being Event of COM (Sigma,P) st A c= B holds
comP . (B \ A) = (comP . B) - (comP . A)
A68:
for A, B being Event of COM (Sigma,P) st A c= B holds
comP . A <= comP . B
A69:
for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds
comP * BSeq is non-decreasing
A72: comP . Omega =
comP . ({} \/ Omega)
.=
P . Omega
by A5, A1, PROB_1:5
.=
1
by PROB_1:def 8
;
A73:
for A being Event of COM (Sigma,P) holds comP . A <= 1
A74:
for BSeq being SetSequence of COM (Sigma,P)
for n being Element of NAT holds (comP * BSeq) . n <= 1
A75:
for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds
( comP * BSeq is V109() & comP * BSeq is convergent )
for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds
( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) )
then reconsider comP = comP as Probability of COM (Sigma,P) by A48, A72, A52, PROB_2:10;
take
comP
; for B being set st B in Sigma holds
for C being thin of P holds comP . (B \/ C) = P . B
thus
for B being set st B in Sigma holds
for C being thin of P holds comP . (B \/ C) = P . B
by A5; verum