let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f, g be PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: ex A being Element of S st
( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) and
A2: f is nonnegative and
A3: g is nonnegative and
A4: for x being Element of X st x in dom g holds
g . x <= f . x ; :: thesis:
consider G being Functional_Sequence of X,ExtREAL , L being ExtREAL_sequence such that
A5: for n being Nat holds
( G . n is_simple_func_in S & dom (G . n) = dom g ) and
A6: for n being Nat holds G . n is nonnegative and
A7: for n, m being Nat st n <= m holds
for x being Element of X st x in dom g holds
(G . n) . x <= (G . m) . x and
A8: for x being Element of X st x in dom g holds
( G # x is convergent & lim (G # x) = g . x ) and
A9: for n being Nat holds L . n = integral' M,(G . n) and
L is convergent and
A10: integral+ M,g = lim L by A1, A3, Def15;
consider F being Functional_Sequence of X,ExtREAL , K being ExtREAL_sequence such that
A11: for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) and
A12: for n being Nat holds F . n is nonnegative and
A13: 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 and
A14: for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) and
A15: for n being Nat holds K . n = integral' M,(F . n) and
K is convergent and
A16: integral+ M,f = lim K by A1, A2, Def15;
consider A being Element of S such that
A17: A = dom f and
A18: A = dom g and
f is_measurable_on A and
g is_measurable_on A by A1;
A19: for x being Element of X st x in A holds
lim (G # x) = sup (rng (G # x))

proof

let x be Element of X; :: thesis:
assume A20: x in A ; :: thesis:

now

let n, m be Nat; :: thesis:
assume A21: n <= m ; :: thesis:
A22: (G # x) . m = (G . m) . x by Def13;
(G # x) . n = (G . n) . x by Def13;
hence (G # x) . n <= (G # x) . m by A18, A7, A20, A21, A22; :: thesis:

end;

hence lim (G # x) = sup (rng (G # x)) by Th60; :: thesis:

end;

A23: for n0 being Nat holds
( L is convergent & sup (rng L) = lim L )

proof

let n0 be Nat; :: thesis:
set ff = G . n0;
A24: G . n0 is nonnegative by A6;
A25: dom (G . n0) = A by A18, A5;
A26: for x being Element of X st x in dom (G . n0) holds
( G # x is convergent & (G . n0) . x <= lim (G # x) )

proof

let x be Element of X; :: thesis:
assume A27: x in dom (G . n0) ; :: thesis:
A28: (G # x) . n0 <= sup (rng (G # x)) by Th62;
(G . n0) . x = (G # x) . n0 by Def13;
hence ( G # x is convergent & (G . n0) . x <= lim (G # x) ) by A18, A8, A19, A25, A27, A28; :: thesis:

end;

G . n0 is_simple_func_in S by A5;
then consider FF being ExtREAL_sequence such that
A29: for n being Nat holds FF . n = integral' M,(G . n) and
A30: FF is convergent and
A31: sup (rng FF) = lim FF and
integral' M,(G . n0) <= lim FF by A18, A5, A6, A7, A25, A24, A26, Th81;

now

let n be Element of NAT ; :: thesis:
thus FF . n = integral' M,(G . n) by A29
.= L . n by A9 ; :: thesis:

end;

then FF = L by FUNCT_2:113;
hence ( L is convergent & sup (rng L) = lim L ) by A30, A31; :: thesis:

end;

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

proof

let n0 be Nat; :: thesis:
set gg = G . n0;
A32: G . n0 is nonnegative by A6;
A33: dom (G . n0) = A by A18, A5;
A34: for x being Element of X st x in dom (G . n0) holds
( F # x is convergent & (G . n0) . x <= lim (F # x) )

proof

let x be Element of X; :: thesis:
assume A35: x in dom (G . n0) ; :: thesis:
A36: (G # x) . n0 <= sup (rng (G # x)) by Th62;
(G . n0) . x = (G # x) . n0 by Def13;
then (G . n0) . x <= lim (G # x) by A19, A33, A35, A36;
then A37: (G . n0) . x <= g . x by A18, A8, A33, A35;
g . x <= f . x by A1, A4, A17, A33, A35;
then g . x <= lim (F # x) by A17, A14, A33, A35;
hence ( F # x is convergent & (G . n0) . x <= lim (F # x) ) by A17, A14, A33, A35, A37, XXREAL_0:2; :: thesis:

end;

G . n0 is_simple_func_in S by A5;
then consider GG being ExtREAL_sequence such that
A38: for n being Nat holds GG . n = integral' M,(F . n) and
A39: GG is convergent and
A40: sup (rng GG) = lim GG and
A41: integral' M,(G . n0) <= lim GG by A17, A11, A12, A13, A33, A32, A34, Th81;

now

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

end;

then GG = K by FUNCT_2:113;
hence ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K ) by A9, A39, A40, A41; :: thesis:

end;

hence integral+ M,g <= integral+ M,f by A16, A10, A23, Th63; :: thesis: