let X be non empty set ; 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; 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; 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; ( 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
; ( 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; verum