defpred S_{1}[ object , object ] means ex A being Event of Sigma ex r being Real st

( A = $1 & r = $2 & r = (P . (A /\ B)) / (P . B) );

A2: for x being object st x in Sigma holds

ex y being object st

( y in REAL & S_{1}[x,y] )

A4: for x being object st x in Sigma holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A2);

A5: for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B)

.= (P . B) / (P . B) by XBOOLE_1:28

.= 1 by A1, XCMPLX_1:60 ;

A7: for A, C being Event of Sigma st A misses C holds

f . (A \/ C) = (f . A) + (f . C)

( f * ASeq is convergent & lim (f * ASeq) = f . (Intersection ASeq) )

take f ; :: thesis: for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B)

thus for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B) by A5; :: thesis: verum

( A = $1 & r = $2 & r = (P . (A /\ B)) / (P . B) );

A2: for x being object st x in Sigma holds

ex y being object st

( y in REAL & S

proof

consider f being Function of Sigma,REAL such that
let x be object ; :: thesis: ( x in Sigma implies ex y being object st

( y in REAL & S_{1}[x,y] ) )

assume x in Sigma ; :: thesis: ex y being object st

( y in REAL & S_{1}[x,y] )

then reconsider x = x as Event of Sigma ;

consider y being object such that

A3: y = (P . (x /\ B)) / (P . B) ;

take y ; :: thesis: ( y in REAL & S_{1}[x,y] )

thus ( y in REAL & S_{1}[x,y] )
by A3; :: thesis: verum

end;( y in REAL & S

assume x in Sigma ; :: thesis: ex y being object st

( y in REAL & S

then reconsider x = x as Event of Sigma ;

consider y being object such that

A3: y = (P . (x /\ B)) / (P . B) ;

take y ; :: thesis: ( y in REAL & S

thus ( y in REAL & S

A4: for x being object st x in Sigma holds

S

A5: for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B)

proof

then A6: f . Omega =
(P . (([#] Sigma) /\ B)) / (P . B)
let A be Event of Sigma; :: thesis: f . A = (P . (A /\ B)) / (P . B)

ex C being Event of Sigma ex r1 being Real st

( C = A & r1 = f . A & r1 = (P . (C /\ B)) / (P . B) ) by A4;

hence f . A = (P . (A /\ B)) / (P . B) ; :: thesis: verum

end;ex C being Event of Sigma ex r1 being Real st

( C = A & r1 = f . A & r1 = (P . (C /\ B)) / (P . B) ) by A4;

hence f . A = (P . (A /\ B)) / (P . B) ; :: thesis: verum

.= (P . B) / (P . B) by XBOOLE_1:28

.= 1 by A1, XCMPLX_1:60 ;

A7: for A, C being Event of Sigma st A misses C holds

f . (A \/ C) = (f . A) + (f . C)

proof

A9:
for A being Event of Sigma holds 0 <= f . A
let A, C be Event of Sigma; :: thesis: ( A misses C implies f . (A \/ C) = (f . A) + (f . C) )

assume A misses C ; :: thesis: f . (A \/ C) = (f . A) + (f . C)

then A8: A /\ B misses C /\ B by XBOOLE_1:76;

thus f . (A \/ C) = (P . ((A \/ C) /\ B)) / (P . B) by A5

.= (P . ((A /\ B) \/ (C /\ B))) / (P . B) by XBOOLE_1:23

.= ((P . (A /\ B)) + (P . (C /\ B))) / (P . B) by A8, PROB_1:def 8

.= ((P . (A /\ B)) / (P . B)) + ((P . (C /\ B)) / (P . B)) by XCMPLX_1:62

.= ((P . (A /\ B)) / (P . B)) + (f . C) by A5

.= (f . A) + (f . C) by A5 ; :: thesis: verum

end;assume A misses C ; :: thesis: f . (A \/ C) = (f . A) + (f . C)

then A8: A /\ B misses C /\ B by XBOOLE_1:76;

thus f . (A \/ C) = (P . ((A \/ C) /\ B)) / (P . B) by A5

.= (P . ((A /\ B) \/ (C /\ B))) / (P . B) by XBOOLE_1:23

.= ((P . (A /\ B)) + (P . (C /\ B))) / (P . B) by A8, PROB_1:def 8

.= ((P . (A /\ B)) / (P . B)) + ((P . (C /\ B)) / (P . B)) by XCMPLX_1:62

.= ((P . (A /\ B)) / (P . B)) + (f . C) by A5

.= (f . A) + (f . C) by A5 ; :: thesis: verum

proof

for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
let A be Event of Sigma; :: thesis: 0 <= f . A

0 <= P . (A /\ B) by PROB_1:def 8;

then 0 <= (P . (A /\ B)) / (P . B) by A1;

hence 0 <= f . A by A5; :: thesis: verum

end;0 <= P . (A /\ B) by PROB_1:def 8;

then 0 <= (P . (A /\ B)) / (P . B) by A1;

hence 0 <= f . A by A5; :: thesis: verum

( f * ASeq is convergent & lim (f * ASeq) = f . (Intersection ASeq) )

proof

then reconsider f = f as Probability of Sigma by A9, A6, A7, PROB_1:def 8;
let ASeq be SetSequence of Sigma; :: thesis: ( ASeq is non-ascending implies ( f * ASeq is convergent & lim (f * ASeq) = f . (Intersection ASeq) ) )

assume A10: ASeq is non-ascending ; :: thesis: ( f * ASeq is convergent & lim (f * ASeq) = f . (Intersection ASeq) )

consider BSeq being SetSequence of Sigma such that

A11: for n being Nat holds BSeq . n = (ASeq . n) /\ B by Th3;

A12: dom (f * ASeq) = NAT by FUNCT_2:def 1;

then A16: P * BSeq is convergent by PROB_1:def 8;

dom (P * BSeq) = NAT by FUNCT_2:def 1;

then A17: f * ASeq = ((P . B) ") (#) (P * BSeq) by A12, A13, VALUED_1:def 5;

hence f * ASeq is convergent by A16, SEQ_2:7; :: thesis: lim (f * ASeq) = f . (Intersection ASeq)

lim (P * BSeq) = P . (Intersection BSeq) by A15, PROB_1:def 8;

hence lim (f * ASeq) = ((P . B) ") * (P . (@Intersection BSeq)) by A17, A16, SEQ_2:8

.= (P . (@Intersection BSeq)) / (P . B) by XCMPLX_0:def 9

.= (P . ((@Intersection ASeq) /\ B)) / (P . B) by A11, Th5

.= f . (Intersection ASeq) by A5 ;

:: thesis: verum

end;assume A10: ASeq is non-ascending ; :: thesis: ( f * ASeq is convergent & lim (f * ASeq) = f . (Intersection ASeq) )

consider BSeq being SetSequence of Sigma such that

A11: for n being Nat holds BSeq . n = (ASeq . n) /\ B by Th3;

A12: dom (f * ASeq) = NAT by FUNCT_2:def 1;

A13: now :: thesis: for n being object st n in dom (f * ASeq) holds

(f * ASeq) . n = ((P . B) ") * ((P * BSeq) . n)

A15:
BSeq is non-ascending
by A10, A11, Th4;(f * ASeq) . n = ((P . B) ") * ((P * BSeq) . n)

let n be object ; :: thesis: ( n in dom (f * ASeq) implies (f * ASeq) . n = ((P . B) ") * ((P * BSeq) . n) )

assume A14: n in dom (f * ASeq) ; :: thesis: (f * ASeq) . n = ((P . B) ") * ((P * BSeq) . n)

then reconsider n1 = n as Element of NAT by FUNCT_2:def 1;

thus (f * ASeq) . n = f . (ASeq . n) by A12, A14, FUNCT_2:15

.= (P . ((ASeq . n1) /\ B)) / (P . B) by A5

.= (P . (BSeq . n)) / (P . B) by A11

.= ((P * BSeq) . n) / (P . B) by A12, A14, FUNCT_2:15

.= ((P . B) ") * ((P * BSeq) . n) by XCMPLX_0:def 9 ; :: thesis: verum

end;assume A14: n in dom (f * ASeq) ; :: thesis: (f * ASeq) . n = ((P . B) ") * ((P * BSeq) . n)

then reconsider n1 = n as Element of NAT by FUNCT_2:def 1;

thus (f * ASeq) . n = f . (ASeq . n) by A12, A14, FUNCT_2:15

.= (P . ((ASeq . n1) /\ B)) / (P . B) by A5

.= (P . (BSeq . n)) / (P . B) by A11

.= ((P * BSeq) . n) / (P . B) by A12, A14, FUNCT_2:15

.= ((P . B) ") * ((P * BSeq) . n) by XCMPLX_0:def 9 ; :: thesis: verum

then A16: P * BSeq is convergent by PROB_1:def 8;

dom (P * BSeq) = NAT by FUNCT_2:def 1;

then A17: f * ASeq = ((P . B) ") (#) (P * BSeq) by A12, A13, VALUED_1:def 5;

hence f * ASeq is convergent by A16, SEQ_2:7; :: thesis: lim (f * ASeq) = f . (Intersection ASeq)

lim (P * BSeq) = P . (Intersection BSeq) by A15, PROB_1:def 8;

hence lim (f * ASeq) = ((P . B) ") * (P . (@Intersection BSeq)) by A17, A16, SEQ_2:8

.= (P . (@Intersection BSeq)) / (P . B) by XCMPLX_0:def 9

.= (P . ((@Intersection ASeq) /\ B)) / (P . B) by A11, Th5

.= f . (Intersection ASeq) by A5 ;

:: thesis: verum

take f ; :: thesis: for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B)

thus for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B) by A5; :: thesis: verum