defpred S₁[ 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₁[x,y] )

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

end;

consider f being Function of Sigma,REAL such that
A4: for x being object 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)

let A be Event of Sigma; :: thesis:
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:

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)

let A, C be Event of Sigma; :: thesis:
assume A misses C ; :: thesis:
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:

end;

let A be Event of Sigma; :: thesis:
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:

end;

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

let ASeq be SetSequence of Sigma; :: thesis:
assume A10: ASeq is non-ascending ; :: thesis:
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;

let n be object ; :: thesis:
assume A14: n in dom (f * ASeq) ; :: thesis:
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:

end;

end;

then reconsider f = f as Probability of Sigma by A9, A6, A7, PROB_1:def 8;
take f ; :: thesis:
thus for A being Event of Sigma holds f . A = (P . (A /\ B)) / (P . B) by A5; :: thesis: