:: deftheorem defines sigma_finite MEASUR11:def 12 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( M is sigma_finite iff ex E being Set_Sequence of S st
( ( for n being Nat holds M . (E . n) < +infty ) & Union E = X ) );