theorem Th19: :: MESFUN13:23

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
( M . (eq_dom (f,+infty)) = 0 & M . (eq_dom (f,-infty)) = 0 & f is_a.e.finite M & ( for r being Real st r > 0 holds
M . (great_eq_dom (|.f.|,r)) < +infty ) )