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
( K is convergent & sup (rng K) = lim K & L . n0 <= lim K )

let n0 be Nat; :: thesis:
reconsider g = G . n0 as PartFunc of X,ExtREAL ;
A10: dom g = A by A4;
for x being Element of X st x in dom g holds
( F # x is convergent & g . x <= lim (F # x) )

let x be Element of X; :: thesis:
assume x in dom g ; :: thesis:
then A11: x in A by A4;

let n, m be Nat; :: thesis:
assume A12: n <= m ; :: thesis:
( (G # x) . n = (G . n) . x & (G # x) . m = (G . m) . x ) by Def13;
hence (G # x) . n <= (G # x) . m by A6, A11, A12; :: thesis:

end;

then A13: lim (G # x) = sup (rng (G # x)) by Th60;
A14: g . x = (G # x) . n0 by Def13;
(G # x) . n0 <= sup (rng (G # x)) by Th62;
hence ( F # x is convergent & g . x <= lim (F # x) ) by A7, A11, A13, A14; :: thesis:

end;

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 A1, A2, A3, A4, A5, A10;
then consider GG being ExtREAL_sequence such that
A15: ( ( for n being Nat holds GG . n = integral' M,(F . n) ) & GG is convergent & sup (rng GG) = lim GG & integral' M,g <= lim GG ) by Th81;
GG = K

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

end;

hence GG = K by FUNCT_2:113; :: thesis:

end;

hence ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K ) by A8, A15; :: thesis:

end;

A16: for n0 being Nat holds
( L is convergent & sup (rng L) = lim L & K . n0 <= lim L )

let n0 be Nat; :: thesis:
reconsider f = F . n0 as PartFunc of X,ExtREAL ;
A17: dom f = A by A1;
for x being Element of X st x in dom f holds
( G # x is convergent & f . x <= lim (G # x) )

let x be Element of X; :: thesis:
assume x in dom f ; :: thesis:
then A18: x in A by A1;
A19: f . x = (F # x) . n0 by Def13;

let n, m be Nat; :: thesis:
assume A20: n <= m ; :: thesis:
( (F # x) . n = (F . n) . x & (F # x) . m = (F . m) . x ) by Def13;
hence (F # x) . n <= (F # x) . m by A3, A18, A20; :: thesis:

end;

then A21: lim (F # x) = sup (rng (F # x)) by Th60;
(F # x) . n0 <= sup (rng (F # x)) by Th62;
hence ( G # x is convergent & f . x <= lim (G # x) ) by A7, A18, A19, A21; :: thesis:

end;

then ( f is_simple_func_in S & f is nonnegative & ( for n being Nat holds G . n is_simple_func_in S ) & ( for n being Nat holds dom (G . n) = dom f ) & ( for n being Nat holds G . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(G . n) . x <= (G . m) . x ) & ( for x being Element of X st x in dom f holds
( G # x is convergent & f . x <= lim (G # x) ) ) ) by A1, A2, A4, A5, A6, A17;
then consider FF being ExtREAL_sequence such that
A22: ( ( for n being Nat holds FF . n = integral' M,(G . n) ) & FF is convergent & sup (rng FF) = lim FF & integral' M,f <= lim FF ) by Th81;

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

end;

then FF = L by FUNCT_2:113;
hence ( L is convergent & sup (rng L) = lim L & K . n0 <= lim L ) by A8, A22; :: thesis:

end;

hence ( K is convergent & L is convergent ) by A9; :: thesis:
( lim L <= lim K & lim K <= lim L ) by A9, A16, Th63;
hence lim K = lim L by XXREAL_0:1; :: thesis: