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
A82: for B being set st B in Sigma holds
for C being thin of P holds P1 . (B \/ C) = P . B and
A83: 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 set st x in COM (Sigma,P) holds
P1 . x = P2 . x

proof

let x be set ; :: 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
A84: ( B in Sigma & ex C being thin of P st x = B \/ C ) by Def5;
P1 . x = P . B by A82, A84
.= P2 . x by A83, A84 ;
hence P1 . x = P2 . x ; :: thesis: verum

end;

hence P1 = P2 by FUNCT_2:12; :: thesis: verum