theorem :: MESFUN7C:36

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,COMPLEX st f is_integrable_on M holds
ex F being sequence of S st
( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds
( F . n in S & M . (F . n) < +infty ) ) )