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

now

let n, m be Nat; :: thesis: ( n <= m implies (G # x) . n <= (G # x) . m )
assume A7: n <= m ; :: thesis: (G # x) . n <= (G # x) . m
( (G # x) . n = (G . n) . x & (G # x) . m = (G . m) . x ) by Def13;
hence (G # x) . n <= (G # x) . m by A2, A4, A6, A7; :: thesis: verum

end;

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

end;

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

proof

let n0 be Nat; :: thesis: ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K )
set gg = G . n0;
A9: ( dom (G . n0) = A & G . n0 is_simple_func_in S & G . n0 is nonnegative ) by A2, A4;
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: ( x in dom (G . n0) implies ( F # x is convergent & (G . n0) . x <= lim (F # x) ) )
assume A10: x in dom (G . n0) ; :: thesis: ( F # x is convergent & (G . n0) . x <= lim (F # x) )
( (G . n0) . x = (G # x) . n0 & (G # x) . n0 <= sup (rng (G # x)) ) by Def13, Th62;
then ( (G . n0) . x <= lim (G # x) & g . x <= f . x ) by A1, A2, A5, A9, A10;
then ( (G . n0) . x <= g . x & g . x <= lim (F # x) ) by A2, A3, A4, A9, A10;
hence ( F # x is convergent & (G . n0) . x <= lim (F # x) ) by A2, A3, A9, A10, XXREAL_0:2; :: thesis: verum

end;

then consider GG being ExtREAL_sequence such that
A11: ( ( for n being Nat holds GG . n = integral' M,(F . n) ) & GG is convergent & sup (rng GG) = lim GG & integral' M,(G . n0) <= lim GG ) by A2, A3, A9, Th81;

now

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

end;

then GG = K by FUNCT_2:113;
hence ( K is convergent & sup (rng K) = lim K & L . n0 <= lim K ) by A4, A11; :: thesis: verum

end;

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

proof

let n0 be Nat; :: thesis: ( L is convergent & sup (rng L) = lim L )
set ff = G . n0;
A12: ( dom (G . n0) = A & G . n0 is_simple_func_in S & G . n0 is nonnegative ) by A2, A4;
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: ( x in dom (G . n0) implies ( G # x is convergent & (G . n0) . x <= lim (G # x) ) )
assume A13: x in dom (G . n0) ; :: thesis: ( G # x is convergent & (G . n0) . x <= lim (G # x) )
( (G . n0) . x = (G # x) . n0 & (G # x) . n0 <= sup (rng (G # x)) ) by Def13, Th62;
hence ( G # x is convergent & (G . n0) . x <= lim (G # x) ) by A2, A4, A5, A12, A13; :: thesis: verum

end;

then consider FF being ExtREAL_sequence such that
A14: ( ( for n being Nat holds FF . n = integral' M,(G . n) ) & FF is convergent & sup (rng FF) = lim FF & integral' M,(G . n0) <= lim FF ) by A2, A4, A12, Th81;

now

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

end;

then FF = L by FUNCT_2:113;
hence ( L is convergent & sup (rng L) = lim L ) by A14; :: thesis: verum

end;

hence integral+ M,g <= integral+ M,f by A3, A4, A8, Th63; :: thesis: verum