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_measurable_on A by A1, Def17;
A4: integral+ M,(max+ f) <> +infty by A1, Def17;
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, Th85, MESFUNC2:27;
then reconsider maxf1 = integral+ M,(max+ f) as Real by A4, XXREAL_0:14;
A7: max+ f is_measurable_on A by A3, MESFUNC2:27;
A8: integral+ M,(max- f) <> +infty by A1, Def17;
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, Th85, MESFUNC2:28;
then reconsider maxf2 = integral+ M,(max- f) as Real by A8, XXREAL_0:14;
(integral+ M,(max+ f)) - (integral+ M,(max- f)) = maxf1 - maxf2 by SUPINF_2:5;
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, Th85, MESFUNC2:28, XXREAL_0:9, XXREAL_0:12; :: thesis: verum