let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
|.(Integral M,f).| <= Integral M,|.f.|
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
|.(Integral M,f).| <= Integral M,|.f.|
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_integrable_on M holds
|.(Integral M,f).| <= Integral M,|.f.|
let f be PartFunc of X,ExtREAL ; :: thesis: ( f is_integrable_on M implies |.(Integral M,f).| <= Integral M,|.f.| )
assume A1: f is_integrable_on M ; :: thesis: |.(Integral M,f).| <= Integral M,|.f.|
consider A being Element of S such that
A2: ( A = dom f & f is_measurable_on A ) by A1, Def17;
A3: ( 0 <= integral+ M,(max+ f) & 0 <= integral+ M,(max- f) & -infty < Integral M,f & Integral M,f < +infty & integral+ M,(max+ f) <> +infty & integral+ M,(max- f) <> +infty ) by A1, Def17, Th102;
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 |.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;

A6: ( dom f = dom (max+ f) & dom f = dom (max- f) ) by MESFUNC2:def 2, MESFUNC2:def 3;
A7: ( max+ f is nonnegative & max- f is nonnegative ) by Lm1;
A8: ( max+ f is_measurable_on A & max- f is_measurable_on A ) by A2, MESFUNC2:27, MESFUNC2:28;
then A9: ( 0 <= integral+ M,(max+ f) & 0 <= integral+ M,(max- f) ) by A2, A6, A7, Th85;
|.f.| = (max+ f) + (max- f) by MESFUNC2:26;
then A10: Integral M,|.f.| = integral+ M,((max+ f) + (max- f)) by A4, B5, Th94, SUPINF_2:71
.= (integral+ M,(max+ f)) + (integral+ M,(max- f)) by A2, A6, A7, A8, Lm11 ;
|.((integral+ M,(max+ f)) - (integral+ M,(max- f))).| <= |.(integral+ M,(max+ f)).| + |.(integral+ M,(max- f)).| by A3, EXTREAL2:69;
then |.(Integral M,f).| <= (integral+ M,(max+ f)) + |.(integral+ M,(max- f)).| by A9, EXTREAL1:def 3;
hence |.(Integral M,f).| <= Integral M,|.f.| by A9, A10, EXTREAL1:def 3; :: thesis: verum