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 inREAL & S1[x,y] )
consider f being Function of Sigma,REAL such that A4:
for x being object st x in Sigma holds S1[x,f . x]
fromFUNCT_2:sch 1(A2); A5:
for A being Event of Sigma holds f . A =(P .(A /\ B))/(P . B)