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
A49: for B being set st B in S holds
for C being thin of M holds M1 . (B \/ C) = M . B and
A50: 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 set st x in COM S,M holds
M1 . x = M2 . x

proof

let x be set ; :: 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
A51: ( B in S & ex C being thin of M st x = B \/ C ) by Def4;
M1 . x = M . B by A49, A51
.= M2 . x by A50, A51 ;
hence M1 . x = M2 . x ; :: thesis: verum

end;

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