theorem Th28: :: MESFUNC8:28

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st M . E < +infty & dom (f . 0) = E & ( for n being Nat holds
( f . n is_measurable_on E & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
for r, e being Real st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )