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 A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
|.(f . x).| <= g . x ) holds
( f is_integrable_on M & Integral M,|.f.| <= Integral M,g )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
|.(f . x).| <= g . x ) holds
( f is_integrable_on M & Integral M,|.f.| <= Integral M,g )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
|.(f . x).| <= g . x ) holds
( f is_integrable_on M & Integral M,|.f.| <= Integral M,g )
let f, g be PartFunc of X,ExtREAL ; :: thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
|.(f . x).| <= g . x ) implies ( f is_integrable_on M & Integral M,|.f.| <= Integral M,g ) )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) 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: ( f is_integrable_on M & Integral M,|.f.| <= Integral M,g )
A5: ex AA being Element of S st
( AA = dom g & g is_measurable_on AA ) by A3, Def17;

A6: now

let x be set ; :: thesis: ( x in dom g implies 0 <= g . x )
assume x in dom g ; :: thesis: 0 <= g . x
then |.(f . x).| <= g . x by A2, A4;
hence 0 <= g . x by EXTREAL2:51; :: thesis: verum

end;

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

now

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

end;

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

A12: now

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

end;

then A15: |.f.| = max+ |.f.| by A11, FUNCT_1:9;
consider A being Element of S such that
A16: A = dom f and
A17: f is_measurable_on A by A1;
A18: |.f.| is_measurable_on A by A16, A17, MESFUNC2:29;
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

proof

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

end;

A22: now

let x be set ; :: thesis: ( x in dom |.f.| implies 0 <= |.f.| . x )
assume x in dom |.f.| ; :: thesis: 0 <= |.f.| . x
then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;
hence 0 <= |.f.| . x by EXTREAL2:51; :: thesis: verum

end;

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

now

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

end;

then A25: integral+ M,(max- |.f.|) = 0 by A19, A18, A24, Th93, MESFUNC2:28;
integral+ M,(max+ g) < +infty by A3, Def17;
then integral+ M,(max+ |.f.|) < +infty by A15, A10, A23, XXREAL_0:2;
then |.f.| is_integrable_on M by A19, A18, A25, Def17;
hence f is_integrable_on M by A1, Th106; :: thesis: Integral M,|.f.| <= Integral M,g
Integral M,g = integral+ M,g by A5, A6, Th94, SUPINF_2:71;
hence Integral M,|.f.| <= Integral M,g by A19, A18, A22, A23, Th94, SUPINF_2:71; :: thesis: verum