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

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

hence
P1 = P2
by Th9; :: thesis: verumlet 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;thus P1 . A = (P . (A /\ B)) / (P . B) by A18

.= P2 . A by A19 ; :: thesis: verum