theorem :: MESFUNC9:48

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is E -measurable holds
ex g being Functional_Sequence of X,ExtREAL st
( g is additive & ( for n being Nat holds
( g . n is_simple_func_in S & g . n is nonnegative & g . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( g # x is summable & f . x = Sum (g # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((g . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )