:: deftheorem defines sigma-additive MEASURE1:def 6 :
for X being set
for S being SigmaField of X
for F being Function of S,ExtREAL holds
( F is sigma-additive iff for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s)) );