theorem :: MESFUNC9:47

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 Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is E -measurable & F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )