theorem Th74: :: MESFUNC5:74

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for g being PartFunc of X,ExtREAL
for F being Functional_Sequence of X,ExtREAL
for L being ExtREAL_sequence st g is_simple_func_in S & ( for x being object st x in dom g holds
0 < g . x ) & ( for n being Nat holds F . n is_simple_func_in S ) & ( for n being Nat holds dom (F . n) = dom g ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom g holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) ) ) & ( for n being Nat holds L . n = integral' (M,(F . n)) ) holds
( L is convergent & integral' (M,g) <= lim L )