theorem Th21: :: MESFUN14:21

for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL st f is bounded & A c= dom f & vol A > 0 holds
ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st
( A = dom (F . 0) & ( for n being Nat holds
( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds
for x being Element of REAL st x in A holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )