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

for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

let A be Element of S; :: thesis: ( f is_integrable_on M implies ( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M ) )

A1: max+ f is nonnegative by Lm1;

assume A2: f is_integrable_on M ; :: thesis: ( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

then consider E being Element of S such that

A3: E = dom f and

A4: f is E -measurable ;

A5: max+ f is E -measurable by A4, MESFUNC2:25;

A6: f is E /\ A -measurable by A4, MESFUNC1:30, XBOOLE_1:17;

(dom f) /\ (E /\ A) = E /\ A by A3, XBOOLE_1:17, XBOOLE_1:28;

then f | (E /\ A) is E /\ A -measurable by A6, Th42;

then (f | E) | A is E /\ A -measurable by RELAT_1:71;

then A7: f | A is E /\ A -measurable by A3, GRFUNC_1:23;

A8: integral+ (M,(max- f)) < +infty by A2;

A9: max- f is nonnegative by Lm1;

A10: integral+ (M,(max+ f)) < +infty by A2;

A11: (max+ f) | (E /\ A) = ((max+ f) | E) | A by RELAT_1:71;

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

then (max+ f) | E = max+ f by A3, GRFUNC_1:23;

then A13: integral+ (M,((max+ f) | A)) <= integral+ (M,(max+ f)) by A3, A5, A12, A1, A11, Th83, XBOOLE_1:17;

then integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) by Th28;

then A14: integral+ (M,(max+ (f | A))) < +infty by A10, XXREAL_0:2;

A15: max- f is E -measurable by A3, A4, MESFUNC2:26;

A16: (max- f) | (E /\ A) = ((max- f) | E) | A by RELAT_1:71;

A17: dom f = dom (max- f) by MESFUNC2:def 3;

then (max- f) | E = max- f by A3, GRFUNC_1:23;

then A18: integral+ (M,((max- f) | A)) <= integral+ (M,(max- f)) by A3, A15, A17, A9, A16, Th83, XBOOLE_1:17;

then integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) by Th28;

then A19: integral+ (M,(max- (f | A))) < +infty by A8, XXREAL_0:2;

E /\ A = dom (f | A) by A3, RELAT_1:61;

hence ( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M ) by A13, A18, A7, A14, A19, Th28; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st f is_integrable_on M holds

( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

let A be Element of S; :: thesis: ( f is_integrable_on M implies ( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M ) )

A1: max+ f is nonnegative by Lm1;

assume A2: f is_integrable_on M ; :: thesis: ( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M )

then consider E being Element of S such that

A3: E = dom f and

A4: f is E -measurable ;

A5: max+ f is E -measurable by A4, MESFUNC2:25;

A6: f is E /\ A -measurable by A4, MESFUNC1:30, XBOOLE_1:17;

(dom f) /\ (E /\ A) = E /\ A by A3, XBOOLE_1:17, XBOOLE_1:28;

then f | (E /\ A) is E /\ A -measurable by A6, Th42;

then (f | E) | A is E /\ A -measurable by RELAT_1:71;

then A7: f | A is E /\ A -measurable by A3, GRFUNC_1:23;

A8: integral+ (M,(max- f)) < +infty by A2;

A9: max- f is nonnegative by Lm1;

A10: integral+ (M,(max+ f)) < +infty by A2;

A11: (max+ f) | (E /\ A) = ((max+ f) | E) | A by RELAT_1:71;

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

then (max+ f) | E = max+ f by A3, GRFUNC_1:23;

then A13: integral+ (M,((max+ f) | A)) <= integral+ (M,(max+ f)) by A3, A5, A12, A1, A11, Th83, XBOOLE_1:17;

then integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) by Th28;

then A14: integral+ (M,(max+ (f | A))) < +infty by A10, XXREAL_0:2;

A15: max- f is E -measurable by A3, A4, MESFUNC2:26;

A16: (max- f) | (E /\ A) = ((max- f) | E) | A by RELAT_1:71;

A17: dom f = dom (max- f) by MESFUNC2:def 3;

then (max- f) | E = max- f by A3, GRFUNC_1:23;

then A18: integral+ (M,((max- f) | A)) <= integral+ (M,(max- f)) by A3, A15, A17, A9, A16, Th83, XBOOLE_1:17;

then integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) by Th28;

then A19: integral+ (M,(max- (f | A))) < +infty by A8, XXREAL_0:2;

E /\ A = dom (f | A) by A3, RELAT_1:61;

hence ( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) & integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) & f | A is_integrable_on M ) by A13, A18, A7, A14, A19, Th28; :: thesis: verum