let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL st A = dom f & f is A -measurable & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

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

for A being Element of S

for f being PartFunc of X,ExtREAL st A = dom f & f is A -measurable & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

let M be sigma_Measure of S; :: thesis: for A being Element of S

for f being PartFunc of X,ExtREAL st A = dom f & f is A -measurable & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

let A be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st A = dom f & f is A -measurable & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

let f be PartFunc of X,ExtREAL; :: thesis: ( A = dom f & f is A -measurable & f is nonnegative implies ( Integral (M,f) in REAL iff f is_integrable_on M ) )

assume A1: ( A = dom f & f is A -measurable & f is nonnegative ) ; :: thesis: ( Integral (M,f) in REAL iff f is_integrable_on M )

for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL st A = dom f & f is A -measurable & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

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

for A being Element of S

for f being PartFunc of X,ExtREAL st A = dom f & f is A -measurable & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

let M be sigma_Measure of S; :: thesis: for A being Element of S

for f being PartFunc of X,ExtREAL st A = dom f & f is A -measurable & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

let A be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st A = dom f & f is A -measurable & f is nonnegative holds

( Integral (M,f) in REAL iff f is_integrable_on M )

let f be PartFunc of X,ExtREAL; :: thesis: ( A = dom f & f is A -measurable & f is nonnegative implies ( Integral (M,f) in REAL iff f is_integrable_on M ) )

assume A1: ( A = dom f & f is A -measurable & f is nonnegative ) ; :: thesis: ( Integral (M,f) in REAL iff f is_integrable_on M )

A2: now :: thesis: ( f is_integrable_on M implies Integral (M,f) in REAL )

assume
f is_integrable_on M
; :: thesis: Integral (M,f) in REAL

then ( -infty < Integral (M,f) & Integral (M,f) < +infty ) by MESFUNC5:96;

hence Integral (M,f) in REAL by XXREAL_0:14; :: thesis: verum

end;then ( -infty < Integral (M,f) & Integral (M,f) < +infty ) by MESFUNC5:96;

hence Integral (M,f) in REAL by XXREAL_0:14; :: thesis: verum

now :: thesis: ( Integral (M,f) in REAL implies f is_integrable_on M )

hence
( Integral (M,f) in REAL iff f is_integrable_on M )
by A2; :: thesis: verumassume A3:
Integral (M,f) in REAL
; :: thesis: f is_integrable_on M

A4: ( dom (max- f) = A & max- f is A -measurable ) by A1, MESFUNC2:26, MESFUNC2:def 3;

A5: ( dom (max+ f) = A & max+ f is A -measurable ) by A1, MESFUNC2:25, MESFUNC2:def 2;

for x being Element of X holds 0 <= (max+ f) . x by MESFUNC2:12;

then max+ f is nonnegative by SUPINF_2:39;

then A6: Integral (M,(max+ f)) = integral+ (M,(max+ f)) by A5, MESFUNC5:88;

A7: for x being Element of X st x in dom f holds

(max+ f) . x = f . x

then A9: Integral (M,(max+ f)) < +infty by A3, XXREAL_0:9;

for x being Element of X holds 0 <= (max- f) . x by MESFUNC2:13;

then max- f is nonnegative by SUPINF_2:39;

then A10: Integral (M,(max- f)) = integral+ (M,(max- f)) by A4, MESFUNC5:88;

for x being Element of X st x in dom (max- f) holds

0 = (max- f) . x

hence f is_integrable_on M by A1, A6, A9, A10; :: thesis: verum

end;A4: ( dom (max- f) = A & max- f is A -measurable ) by A1, MESFUNC2:26, MESFUNC2:def 3;

A5: ( dom (max+ f) = A & max+ f is A -measurable ) by A1, MESFUNC2:25, MESFUNC2:def 2;

for x being Element of X holds 0 <= (max+ f) . x by MESFUNC2:12;

then max+ f is nonnegative by SUPINF_2:39;

then A6: Integral (M,(max+ f)) = integral+ (M,(max+ f)) by A5, MESFUNC5:88;

A7: for x being Element of X st x in dom f holds

(max+ f) . x = f . x

proof

then
max+ f = f
by A1, A5, PARTFUN1:5;
let x be Element of X; :: thesis: ( x in dom f implies (max+ f) . x = f . x )

A8: f . x >= 0 by A1, SUPINF_2:39;

assume x in dom f ; :: thesis: (max+ f) . x = f . x

then (max+ f) . x = max ((f . x),0) by A1, A5, MESFUNC2:def 2;

hence (max+ f) . x = f . x by A8, XXREAL_0:def 10; :: thesis: verum

end;A8: f . x >= 0 by A1, SUPINF_2:39;

assume x in dom f ; :: thesis: (max+ f) . x = f . x

then (max+ f) . x = max ((f . x),0) by A1, A5, MESFUNC2:def 2;

hence (max+ f) . x = f . x by A8, XXREAL_0:def 10; :: thesis: verum

then A9: Integral (M,(max+ f)) < +infty by A3, XXREAL_0:9;

for x being Element of X holds 0 <= (max- f) . x by MESFUNC2:13;

then max- f is nonnegative by SUPINF_2:39;

then A10: Integral (M,(max- f)) = integral+ (M,(max- f)) by A4, MESFUNC5:88;

for x being Element of X st x in dom (max- f) holds

0 = (max- f) . x

proof

then
Integral (M,(max- f)) = 0
by A4, LPSPACE1:22;
let x be Element of X; :: thesis: ( x in dom (max- f) implies 0 = (max- f) . x )

assume x in dom (max- f) ; :: thesis: 0 = (max- f) . x

(max+ f) . x = f . x by A1, A5, A7, PARTFUN1:5;

hence 0 = (max- f) . x by MESFUNC2:19; :: thesis: verum

end;assume x in dom (max- f) ; :: thesis: 0 = (max- f) . x

(max+ f) . x = f . x by A1, A5, A7, PARTFUN1:5;

hence 0 = (max- f) . x by MESFUNC2:19; :: thesis: verum

hence f is_integrable_on M by A1, A6, A9, A10; :: thesis: verum