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 A1: ( 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 ) ) ; :: thesis: ( f is_integrable_on M & Integral M,|.f.| <= Integral M,g )
then consider A being Element of S such that
A2: ( A = dom f & f is_measurable_on A ) ;
consider AA being Element of S such that
A3: ( AA = dom g & g is_measurable_on AA ) by A1, Def17;
A4: ( A = dom |.f.| & |.f.| is_measurable_on A ) by A2, MESFUNC1:def 10, MESFUNC2:29;

B5: 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 A1;
hence 0 <= g . x by EXTREAL2:51; :: thesis: verum

end;

then A5: g is nonnegative by SUPINF_2:71;

B6: 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 A6: |.f.| is nonnegative by SUPINF_2:71;
A7: ( dom |.f.| = dom (max+ |.f.|) & dom |.f.| = dom (max- |.f.|) & dom g = dom (max+ g) ) by MESFUNC2:def 2, MESFUNC2:def 3;

A8: now

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

end;

then A11: |.f.| = max+ |.f.| by A7, FUNCT_1:9;

now

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

end;

then A14: g = max+ g by A7, FUNCT_1:9;

A15: 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 A7, A8;
hence (max- |.f.|) . x = 0 by MESFUNC2:21; :: thesis: verum

end;

A16: integral+ M,(max- |.f.|) = 0 by A4, A7, A15, Th93, MESFUNC2:28;
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 A17: x in dom |.f.| ; :: thesis: |.f.| . x <= g . x
then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;
hence |.f.| . x <= g . x by A1, A2, A4, A17; :: thesis: verum

end;

then A18: integral+ M,|.f.| <= integral+ M,g by A1, A2, A3, A4, A5, A6, Th91;
integral+ M,(max+ g) < +infty by A1, Def17;
then integral+ M,(max+ |.f.|) < +infty by A11, A14, A18, XXREAL_0:2;
then |.f.| is_integrable_on M by A4, A16, Def17;
hence f is_integrable_on M by A1, Th106; :: thesis: Integral M,|.f.| <= Integral M,g
Integral M,g = integral+ M,g by A3, B5, Th94, SUPINF_2:71;
hence Integral M,|.f.| <= Integral M,g by A4, B6, A18, Th94, SUPINF_2:71; :: thesis: verum