let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A being Element of COM (Sigma,P)
for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2
let P be Probability of Sigma; :: thesis: for A being Element of COM (Sigma,P)
for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2
let A be Element of COM (Sigma,P); :: thesis: for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2
let A1, A2 be set ; :: thesis: ( A1 in ProbPart A & A2 in ProbPart A implies P . A1 = P . A2 )
assume that
A1: A1 in ProbPart A and
A2: A2 in ProbPart A ; :: thesis: P . A1 = P . A2
reconsider C1 = A \ A1, C2 = A \ A2 as thin of P by A1, A2, Def7;
A3: A2 c= A by A2, Def7;
A1 c= A by A1, Def7;
then A4: A1 \/ C1 = A by XBOOLE_1:45
.= A2 \/ C2 by A3, XBOOLE_1:45 ;
( A1 in Sigma & A2 in Sigma ) by A1, A2, Def7;
hence P . A1 = P . A2 by A4, Th25; :: thesis: verum