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 A1: ( A1 in ProbPart A & A2 in ProbPart A ) ; :: thesis: P . A1 = P . A2
A2: ( A1 in Sigma & A1 c= A & A \ A1 is thin of P ) by A1, Def7;
A3: ( A2 in Sigma & A2 c= A & A \ A2 is thin of P ) by A1, Def7;
reconsider C1 = A \ A1, C2 = A \ A2 as thin of P by A1, Def7;
A1 \/ C1 = A by A2, XBOOLE_1:45
.= A2 \/ C2 by A3, XBOOLE_1:45 ;
hence P . A1 = P . A2 by A2, A3, Th26; :: thesis: verum