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 A -measurable & g is A -measurable ) 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 A -measurable and
g is A -measurable 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 :: thesis:

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 Th54; :: 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: dom (G . n0) = A by A18, A5;
A25: 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 A26: x in dom (G . n0) ; :: thesis:
A27: (G # x) . n0 <= sup (rng (G # x)) by Th56;
(G . n0) . x = (G # x) . n0 by Def13;
hence ( G # x is convergent & (G . n0) . x <= lim (G # x) ) by A18, A8, A19, A24, A26, A27; :: thesis:

end;

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

now :: thesis:

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

end;

then FF = L by FUNCT_2:63;
hence ( L is convergent & sup (rng L) = lim L ) by A29, A30; :: 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;
A31: G . n0 is nonnegative by A6;
A32: dom (G . n0) = A by A18, A5;
A33: 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 A34: x in dom (G . n0) ; :: thesis:
A35: (G # x) . n0 <= sup (rng (G # x)) by Th56;
(G . n0) . x = (G # x) . n0 by Def13;
then (G . n0) . x <= lim (G # x) by A19, A32, A34, A35;
then A36: (G . n0) . x <= g . x by A18, A8, A32, A34;
g . x <= f . x by A1, A4, A17, A32, A34;
then g . x <= lim (F # x) by A17, A14, A32, A34;
hence ( F # x is convergent & (G . n0) . x <= lim (F # x) ) by A17, A14, A32, A34, A36, XXREAL_0:2; :: thesis:

end;

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

now :: thesis:

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

end;

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

end;

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