for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonpositive holds
ex F being Functional_Sequence of X,ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonpositive ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) )