defpred S1[ 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 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in Sigma implies ex y being object st
( y in REAL & S1[x,y] ) )

assume x in Sigma ; :: thesis: ex y being object st
( y in REAL & S1[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 & S1[x,y] )
thus ( y in REAL & S1[x,y] ) by A3; :: thesis: verum
end;
consider f being Function of Sigma,REAL such that
A4: for x being object st x in Sigma holds
S1[x,f . x] from 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 ;
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
.= ((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 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)
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
.= (P . ((ASeq . n1) /\ B)) / (P . B) by A5
.= (P . (BSeq . n)) / (P . B) by A11
.= ((P * BSeq) . n) / (P . B) by
.= ((P . B) ") * ((P * BSeq) . n) by XCMPLX_0:def 9 ; :: thesis: verum
end;
A15: BSeq is non-ascending by ;
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 ;
hence f * ASeq is convergent by ; :: thesis: lim (f * ASeq) = f . (Intersection ASeq)
lim (P * BSeq) = P . (Intersection BSeq) by ;
hence lim (f * ASeq) = ((P . B) ") * (P . (@Intersection BSeq)) by
.= (P . (@Intersection BSeq)) / (P . B) by XCMPLX_0:def 9
.= (P . ((@Intersection ASeq) /\ B)) / (P . B) by
.= f . (Intersection ASeq) by A5 ;
:: thesis: verum
end;
then reconsider f = f as Probability of Sigma by ;
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