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

( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

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

( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

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

( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M implies ( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty ) )

assume A1: f is_integrable_on M ; :: thesis: ( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

consider A being Element of S such that

A2: A = dom f and

A3: f is A -measurable by A1;

A4: integral+ (M,(max+ f)) <> +infty by A1;

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

A6: max+ f is nonnegative by Lm1;

then -infty <> integral+ (M,(max+ f)) by A2, A3, A5, Th79, MESFUNC2:25;

then reconsider maxf1 = integral+ (M,(max+ f)) as Element of REAL by A4, XXREAL_0:14;

A7: max+ f is A -measurable by A3, MESFUNC2:25;

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

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

A10: max- f is nonnegative by Lm1;

then -infty <> integral+ (M,(max- f)) by A2, A3, A9, Th79, MESFUNC2:26;

then reconsider maxf2 = integral+ (M,(max- f)) as Element of REAL by A8, XXREAL_0:14;

(integral+ (M,(max+ f))) - (integral+ (M,(max- f))) = maxf1 - maxf2 by SUPINF_2:3;

hence ( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty ) by A2, A3, A5, A9, A6, A10, A7, Th79, MESFUNC2:26, XXREAL_0:9, XXREAL_0:12; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_integrable_on M holds

( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

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

( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

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

( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M implies ( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty ) )

assume A1: f is_integrable_on M ; :: thesis: ( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty )

consider A being Element of S such that

A2: A = dom f and

A3: f is A -measurable by A1;

A4: integral+ (M,(max+ f)) <> +infty by A1;

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

A6: max+ f is nonnegative by Lm1;

then -infty <> integral+ (M,(max+ f)) by A2, A3, A5, Th79, MESFUNC2:25;

then reconsider maxf1 = integral+ (M,(max+ f)) as Element of REAL by A4, XXREAL_0:14;

A7: max+ f is A -measurable by A3, MESFUNC2:25;

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

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

A10: max- f is nonnegative by Lm1;

then -infty <> integral+ (M,(max- f)) by A2, A3, A9, Th79, MESFUNC2:26;

then reconsider maxf2 = integral+ (M,(max- f)) as Element of REAL by A8, XXREAL_0:14;

(integral+ (M,(max+ f))) - (integral+ (M,(max- f))) = maxf1 - maxf2 by SUPINF_2:3;

hence ( 0 <= integral+ (M,(max+ f)) & 0 <= integral+ (M,(max- f)) & -infty < Integral (M,f) & Integral (M,f) < +infty ) by A2, A3, A5, A9, A6, A10, A7, Th79, MESFUNC2:26, XXREAL_0:9, XXREAL_0:12; :: thesis: verum