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 & f is A -measurable ) and
A2: dom f = dom g and
A3: g is_integrable_on M and
A4: for x being Element of X st x in dom f holds
|.(f . x).| <= g . x ; :: thesis:
A5: ex AA being Element of S st
( AA = dom g & g is AA -measurable ) by A3;

A6: now :: thesis:

let x be object ; :: thesis:
assume x in dom g ; :: thesis:
then |.(f . x).| <= g . x by A2, A4;
hence 0 <= g . x by EXTREAL1:14; :: thesis:

end;

then A7: g is nonnegative by SUPINF_2:52;
A8: dom g = dom (max+ g) by MESFUNC2:def 2;

let x be object ; :: thesis:
A9: 0 <= g . x by A7, SUPINF_2:51;
assume x in dom g ; :: thesis:
hence (max+ g) . x = max ((g . x),0) by A8, MESFUNC2:def 2
.= g . x by A9, XXREAL_0:def 10 ;
:: thesis:

end;

then A10: g = max+ g by A8, FUNCT_1:2;
A11: dom |.f.| = dom (max+ |.f.|) by MESFUNC2:def 2;

A12: now :: thesis:

let x be object ; :: thesis:
assume A13: x in dom |.f.| ; :: thesis:
then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;
then A14: 0 <= |.f.| . x by EXTREAL1:14;
thus (max+ |.f.|) . x = max ((|.f.| . x),0) by A11, A13, MESFUNC2:def 2
.= |.f.| . x by A14, XXREAL_0:def 10 ; :: thesis:

end;

then A15: |.f.| = max+ |.f.| by A11, FUNCT_1:2;
consider A being Element of S such that
A16: A = dom f and
A17: f is A -measurable by A1;
A18: |.f.| is A -measurable by A16, A17, MESFUNC2:27;
A19: A = dom |.f.| by A16, MESFUNC1:def 10;
A20: for x being Element of X st x in dom |.f.| holds
|.f.| . x <= g . x

let x be Element of X; :: thesis:
assume A21: x in dom |.f.| ; :: thesis:
then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;
hence |.f.| . x <= g . x by A4, A16, A19, A21; :: thesis:

end;

A22: now :: thesis:

let x be object ; :: thesis:
assume x in dom |.f.| ; :: thesis:
then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;
hence 0 <= |.f.| . x by EXTREAL1:14; :: thesis:

end;

then |.f.| is nonnegative by SUPINF_2:52;
then A23: integral+ (M,|.f.|) <= integral+ (M,g) by A2, A16, A5, A19, A18, A7, A20, Th85;
A24: dom |.f.| = dom (max- |.f.|) by MESFUNC2:def 3;

let x be Element of X; :: thesis:
assume x in dom (max- |.f.|) ; :: thesis:
then (max+ |.f.|) . x = |.f.| . x by A24, A12;
hence (max- |.f.|) . x = 0 by MESFUNC2:19; :: thesis:

end;

then A25: integral+ (M,(max- |.f.|)) = 0 by A19, A18, A24, Th87, MESFUNC2:26;
integral+ (M,(max+ g)) < +infty by A3;
then integral+ (M,(max+ |.f.|)) < +infty by A15, A10, A23, XXREAL_0:2;
then |.f.| is_integrable_on M by A19, A18, A25;
hence f is_integrable_on M by A1, Th100; :: thesis:
Integral (M,g) = integral+ (M,g) by A5, A6, Th88, SUPINF_2:52;
hence Integral (M,|.f.|) <= Integral (M,g) by A19, A18, A22, A23, Th88, SUPINF_2:52; :: thesis: