:: deftheorem defines completely-additive MEASURE8:def 11 :
for X being set
for F being Field_Subset of X
for M being Measure of F holds
( M is completely-additive iff for FSets being Sep_Sequence of F st union (rng FSets) in F holds
SUM (M * FSets) = M . (union (rng FSets)) );