let P1, P2 be Probability of COM (Sigma,P); :: thesis: ( ( for B being set st B in Sigma holds
for C being thin of P holds P1 . (B \/ C) = P . B ) & ( for B being set st B in Sigma holds
for C being thin of P holds P2 . (B \/ C) = P . B ) implies P1 = P2 )
assume that
A84: for B being set st B in Sigma holds
for C being thin of P holds P1 . (B \/ C) = P . B and
A85: for B being set st B in Sigma holds
for C being thin of P holds P2 . (B \/ C) = P . B ; :: thesis: P1 = P2
for x being object st x in COM (Sigma,P) holds
P1 . x = P2 . x

proof

let x be object ; :: thesis: ( x in COM (Sigma,P) implies P1 . x = P2 . x )
assume x in COM (Sigma,P) ; :: thesis: P1 . x = P2 . x
then consider B being set such that
A86: ( B in Sigma & ex C being thin of P st x = B \/ C ) by Def5;
P1 . x = P . B by A84, A86
.= P2 . x by A85, A86 ;
hence P1 . x = P2 . x ; :: thesis: verum

end;

hence P1 = P2 ; :: thesis: verum