theorem :: MESFUN11:71

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Functional_Sequence of X,ExtREAL
for E being Element of S st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonpositive & F . n is E -measurable ) ) holds
ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st
for n being Nat holds
( ( for m being Nat holds
( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds
for x being Element of X st x in dom (F . n) holds
((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds
( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )