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.|)
A2: integral+ (M,(max+ f)) <> +infty by A1, Def17;
0 <= integral+ (M,(max+ f)) by A1, Th102;
then A3: |.((integral+ (M,(max+ f))) - (integral+ (M,(max- f)))).| <= |.(integral+ (M,(max+ f))).| + |.(integral+ (M,(max- f))).| by A2, EXTREAL2:69;
A4: dom f = dom (max+ f) by MESFUNC2:def 2;

A5: 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) by MESFUNC2:def 3;
A7: |.f.| = (max+ f) + (max- f) by MESFUNC2:26;
consider A being Element of S such that
A8: A = dom f and
A9: f is_measurable_on A by A1, Def17;
A10: max- f is_measurable_on A by A8, A9, MESFUNC2:28;
A11: max+ f is nonnegative by Lm1;
then 0 <= integral+ (M,(max+ f)) by A8, A9, A4, Th85, MESFUNC2:27;
then A12: |.(Integral (M,f)).| <= (integral+ (M,(max+ f))) + |.(integral+ (M,(max- f))).| by A3, EXTREAL1:def 3;
A13: max+ f is_measurable_on A by A9, MESFUNC2:27;
A14: A = dom |.f.| by A8, MESFUNC1:def 10;
A15: max- f is nonnegative by Lm1;
then A16: 0 <= integral+ (M,(max- f)) by A8, A9, A6, Th85, MESFUNC2:28;
|.f.| is_measurable_on A by A8, A9, MESFUNC2:29;
then Integral (M,|.f.|) = integral+ (M,((max+ f) + (max- f))) by A14, A5, A7, Th94, SUPINF_2:71
.= (integral+ (M,(max+ f))) + (integral+ (M,(max- f))) by A8, A4, A6, A11, A15, A13, A10, Lm10 ;
hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A16, A12, EXTREAL1:def 3; :: thesis: verum