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))) - (integral+ (M,(max- f)))).| <= |.(integral+ (M,(max+ f))).| + |.(integral+ (M,(max- f))).| by EXTREAL1:32;

A3: dom f = dom (max+ f) by MESFUNC2:def 2;

A6: |.f.| = (max+ f) + (max- f) by MESFUNC2:24;

consider A being Element of S such that

A7: A = dom f and

A8: f is A -measurable by A1;

A9: max- f is A -measurable by A7, A8, MESFUNC2:26;

A10: max+ f is nonnegative by Lm1;

then 0 <= integral+ (M,(max+ f)) by A7, A8, A3, Th79, MESFUNC2:25;

then A11: |.(Integral (M,f)).| <= (integral+ (M,(max+ f))) + |.(integral+ (M,(max- f))).| by A2, EXTREAL1:def 1;

A12: max+ f is A -measurable by A8, MESFUNC2:25;

A13: A = dom |.f.| by A7, MESFUNC1:def 10;

A14: max- f is nonnegative by Lm1;

then A15: 0 <= integral+ (M,(max- f)) by A7, A8, A5, Th79, MESFUNC2:26;

|.f.| is A -measurable by A7, A8, MESFUNC2:27;

then Integral (M,|.f.|) = integral+ (M,((max+ f) + (max- f))) by A13, A4, A6, Th88, SUPINF_2:52

.= (integral+ (M,(max+ f))) + (integral+ (M,(max- f))) by A7, A3, A5, A10, A14, A12, A9, Lm10 ;

hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A15, A11, EXTREAL1:def 1; :: thesis: verum

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))) - (integral+ (M,(max- f)))).| <= |.(integral+ (M,(max+ f))).| + |.(integral+ (M,(max- f))).| by EXTREAL1:32;

A3: dom f = dom (max+ f) by MESFUNC2:def 2;

A4: now :: thesis: for x being object st x in dom |.f.| holds

0 <= |.f.| . x

A5:
dom f = dom (max- f)
by MESFUNC2:def 3;0 <= |.f.| . x

let x be object ; :: 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 EXTREAL1:14; :: thesis: verum

end;assume x in dom |.f.| ; :: thesis: 0 <= |.f.| . x

then |.f.| . x = |.(f . x).| by MESFUNC1:def 10;

hence 0 <= |.f.| . x by EXTREAL1:14; :: thesis: verum

A6: |.f.| = (max+ f) + (max- f) by MESFUNC2:24;

consider A being Element of S such that

A7: A = dom f and

A8: f is A -measurable by A1;

A9: max- f is A -measurable by A7, A8, MESFUNC2:26;

A10: max+ f is nonnegative by Lm1;

then 0 <= integral+ (M,(max+ f)) by A7, A8, A3, Th79, MESFUNC2:25;

then A11: |.(Integral (M,f)).| <= (integral+ (M,(max+ f))) + |.(integral+ (M,(max- f))).| by A2, EXTREAL1:def 1;

A12: max+ f is A -measurable by A8, MESFUNC2:25;

A13: A = dom |.f.| by A7, MESFUNC1:def 10;

A14: max- f is nonnegative by Lm1;

then A15: 0 <= integral+ (M,(max- f)) by A7, A8, A5, Th79, MESFUNC2:26;

|.f.| is A -measurable by A7, A8, MESFUNC2:27;

then Integral (M,|.f.|) = integral+ (M,((max+ f) + (max- f))) by A13, A4, A6, Th88, SUPINF_2:52

.= (integral+ (M,(max+ f))) + (integral+ (M,(max- f))) by A7, A3, A5, A10, A14, A12, A9, Lm10 ;

hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A15, A11, EXTREAL1:def 1; :: thesis: verum