let P1, P2 be Probability of Sigma; :: thesis: ( ( for A being Event of Sigma holds P1 . A = (P . (A /\ B)) / (P . B) ) & ( for A being Event of Sigma holds P2 . A = (P . (A /\ B)) / (P . B) ) implies P1 = P2 )
assume that
A18: for A being Event of Sigma holds P1 . A = (P . (A /\ B)) / (P . B) and
A19: for A being Event of Sigma holds P2 . A = (P . (A /\ B)) / (P . B) ; :: thesis: P1 = P2

now :: thesis: for A being Event of Sigma holds P1 . A = P2 . A

let A be Event of Sigma; :: thesis: P1 . A = P2 . A
thus P1 . A = (P . (A /\ B)) / (P . B) by A18
.= P2 . A by A19 ; :: thesis: verum

end;

hence P1 = P2 by Th9; :: thesis: verum