consider F being Functional_Sequence of X,ExtREAL such that
A3: ( ( 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 nonnegative ) & ( 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 ) ) ) by A1, A2, Th70;
reconsider g = F . 0 as PartFunc of X,ExtREAL ;
A4: for x being Element of X st x in dom f holds
( F # x is convergent & g . x <= lim (F # x) )

proof

let x be Element of X; :: thesis: ( x in dom f implies ( F # x is convergent & g . x <= lim (F # x) ) )
assume A5: x in dom f ; :: thesis: ( F # x is convergent & g . x <= lim (F # x) )

now

let n, m be Nat; :: thesis: ( n <= m implies (F # x) . n <= (F # x) . m )
assume A6: n <= m ; :: thesis: (F # x) . n <= (F # x) . m
( (F # x) . n = (F . n) . x & (F # x) . m = (F . m) . x ) by Def13;
hence (F # x) . n <= (F # x) . m by A3, A5, A6; :: thesis: verum

end;

then A7: ( F # x is convergent & lim (F # x) = sup (rng (F # x)) ) by Th60;
g . x = (F # x) . 0 by Def13;
hence ( F # x is convergent & g . x <= lim (F # x) ) by A7, Th62; :: thesis: verum

end;

dom g = dom f by A3;
then ( g is_simple_func_in S & g is nonnegative & ( 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) ) ) ) by A3, A4;
then ex G being ExtREAL_sequence st
( ( for n being Nat holds G . n = integral' M,(F . n) ) & G is convergent & sup (rng G) = lim G & integral' M,g <= lim G ) by Th81;
then consider G being ExtREAL_sequence such that
A8: ( ( for n being Nat holds G . n = integral' M,(F . n) ) & G is convergent & integral' M,g <= lim G ) ;
take lim G ; :: thesis: ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence 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 nonnegative ) & ( 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 ) ) & ( for n being Nat holds K . n = integral' M,(F . n) ) & K is convergent & lim G = lim K )
thus ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence 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 nonnegative ) & ( 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 ) ) & ( for n being Nat holds K . n = integral' M,(F . n) ) & K is convergent & lim G = lim K ) by A3, A8; :: thesis: verum