let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let A be Element of S; :: thesis:
let F, G be Functional_Sequence of X,ExtREAL; :: thesis:
let K, L be ExtREAL_sequence; :: thesis:
assume that
A1: for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = A ) and
A2: for n being Nat holds F . n is nonnegative and
A3: for n, m being Nat st n <= m holds
for x being Element of X st x in A holds
(F . n) . x <= (F . m) . x and
A4: for n being Nat holds
( G . n is_simple_func_in S & dom (G . n) = A ) and
A5: for n being Nat holds G . n is nonnegative and
A6: for n, m being Nat st n <= m holds
for x being Element of X st x in A holds
(G . n) . x <= (G . m) . x and
A7: for x being Element of X st x in A holds
( F # x is convergent & G # x is convergent & lim (F # x) = lim (G # x) ) and
A8: for n being Nat holds
( K . n = integral' (M,(F . n)) & L . n = integral' (M,(G . n)) ) ; :: thesis:
A9: for n0 being Nat holds
( L is convergent & sup (rng L) = lim L & K . n0 <= lim L )

let x be Element of X; :: thesis:
A13: (F # x) . n0 <= sup (rng (F # x)) by Th56;
assume x in dom f ; :: thesis:
then A14: x in A by A1;

let n, m be Nat; :: thesis:
assume A15: n <= m ; :: thesis:
A16: (F # x) . m = (F . m) . x by Def13;
(F # x) . n = (F . n) . x by Def13;
hence (F # x) . n <= (F # x) . m by A3, A14, A15, A16; :: thesis:

end;

then A17: lim (F # x) = sup (rng (F # x)) by Th54;
f . x = (F # x) . n0 by Def13;
hence ( G # x is convergent & f . x <= lim (G # x) ) by A7, A14, A17, A13; :: thesis:

end;

dom f = A by A1;
then consider FF being ExtREAL_sequence such that
A18: for n being Nat holds FF . n = integral' (M,(G . n)) and
A19: FF is convergent and
A20: sup (rng FF) = lim FF and
A21: integral' (M,f) <= lim FF by A4, A5, A6, A12, A10, A11, Th75;

let n be Element of NAT ; :: thesis:
FF . n = integral' (M,(G . n)) by A18;
hence FF . n = L . n by A8; :: thesis:

end;

end;

let x be Element of X; :: thesis:
A26: (G # x) . n0 <= sup (rng (G # x)) by Th56;
assume x in dom g ; :: thesis:
then A27: x in A by A4;

let n, m be Nat; :: thesis:
assume A28: n <= m ; :: thesis:
A29: (G # x) . m = (G . m) . x by Def13;
(G # x) . n = (G . n) . x by Def13;
hence (G # x) . n <= (G # x) . m by A6, A27, A28, A29; :: thesis:

end;

then A30: lim (G # x) = sup (rng (G # x)) by Th54;
g . x = (G # x) . n0 by Def13;
hence ( F # x is convergent & g . x <= lim (F # x) ) by A7, A27, A30, A26; :: thesis:

end;

dom g = A by A4;
then consider GG being ExtREAL_sequence such that
A31: for n being Nat holds GG . n = integral' (M,(F . n)) and
A32: GG is convergent and
A33: sup (rng GG) = lim GG and
A34: integral' (M,g) <= lim GG by A1, A2, A3, A25, A23, A24, Th75;

let n be Element of NAT ; :: thesis:
GG . n = integral' (M,(F . n)) by A31;
hence GG . n = K . n by A8; :: thesis:

end;

end;