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

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

hence
M1 = M2
by FUNCT_2:12; :: thesis: verum
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;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