let M1, M2 be sigma_Measure of (COM (S,M)); :: thesis: ( ( for B being set st B in S holds
for C being thin of M holds M1 . (B \/ C) = M . B ) & ( for B being set st B in S holds
for C being thin of M holds M2 . (B \/ C) = M . B ) implies M1 = M2 )
assume that
A51: for B being set st B in S holds
for C being thin of M holds M1 . (B \/ C) = M . B and
A52: for B being set st B in S holds
for C being thin of M holds M2 . (B \/ C) = M . B ; :: thesis: M1 = M2
for x being object st x in COM (S,M) holds
M1 . x = M2 . x

proof

let x be object ; :: thesis: ( x in COM (S,M) implies M1 . x = M2 . x )
assume x in COM (S,M) ; :: thesis: M1 . x = M2 . x
then consider B being set such that
A53: ( B in S & ex C being thin of M st x = B \/ C ) by Def3;
M1 . x = M . B by A51, A53
.= M2 . x by A52, A53 ;
hence M1 . x = M2 . x ; :: thesis: verum

end;

hence M1 = M2 by FUNCT_2:12; :: thesis: verum