defpred S₁[ set , set ] 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 set st x in Sigma holds
ex y being set st
( y in REAL & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in Sigma implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume x in Sigma ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )
then reconsider x = x as Event of Sigma ;
consider y being set such that
A3: y = (P . (x /\ B)) / (P . B) ;
take y ; :: thesis: ( y in REAL & S₁[x,y] )
thus ( y in REAL & S₁[x,y] ) by A3; :: thesis: verum

end;

consider f being Function of Sigma,REAL such that
A4: for x being set st x in Sigma holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
A5: for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B)

proof

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;

then A6: f . Omega = (P . (([#] Sigma) /\ 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)

proof

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;

A9: for A being Event of Sigma holds 0 <= f . A

proof

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;

for ASeq being SetSequence of Sigma st ASeq is non-ascending holds
( f * ASeq is convergent & lim (f * ASeq) = f . (Intersection ASeq) )

proof

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 Element of NAT holds BSeq . n = (ASeq . n) /\ B by Th9;
A12: dom (f * ASeq) = NAT by FUNCT_2:def 1;

A13: now

let n be set ; :: 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;

A15: BSeq is non-ascending by A10, A11, Th10;
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, Th12
.= f . (Intersection ASeq) by A5 ;
:: thesis: verum

end;

then reconsider f = f as Probability of Sigma by A9, A6, A7, PROB_1:def 8;
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