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_measurable_on A & 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_measurable_on A & 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_measurable_on A & 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_measurable_on A & 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_measurable_on A & f is nonnegative implies ( Integral M,f in REAL iff f is_integrable_on M ) )
assume AS: ( A = dom f & f is_measurable_on A & f is nonnegative ) ; :: thesis: ( Integral M,f in REAL iff f is_integrable_on M )

H1: now

assume f is_integrable_on M ; :: thesis: Integral M,f in REAL
then ( -infty < Integral M,f & Integral M,f < +infty ) by MESFUNC5:102;
hence Integral M,f in REAL by XXREAL_0:14; :: thesis: verum

end;

now

assume P3: Integral M,f in REAL ; :: thesis: f is_integrable_on M
Q0: ( dom (max- f) = A & max- f is_measurable_on A ) by AS, MESFUNC2:28, MESFUNC2:def 3;
Q1: ( dom (max+ f) = A & max+ f is_measurable_on A ) by AS, MESFUNC2:27, MESFUNC2:def 2;
for x being Element of X holds 0 <= (max+ f) . x by MESFUNC2:14;
then max+ f is nonnegative by SUPINF_2:58;
then Q2: Integral M,(max+ f) = integral+ M,(max+ f) by Q1, MESFUNC5:94;
Q2a: for x being Element of X st x in dom f holds
(max+ f) . x = f . x

proof

let x be Element of X; :: thesis: ( x in dom f implies (max+ f) . x = f . x )
A3: f . x >= 0 by AS, SUPINF_2:58;
assume x in dom f ; :: thesis: (max+ f) . x = f . x
then (max+ f) . x = max (f . x),0 by AS, Q1, MESFUNC2:def 2;
hence (max+ f) . x = f . x by A3, XXREAL_0:def 10; :: thesis: verum

end;

then max+ f = f by AS, Q1, PARTFUN1:34;
then Q4: Integral M,(max+ f) < +infty by P3, XXREAL_0:9;
for x being Element of X holds 0 <= (max- f) . x by MESFUNC2:15;
then max- f is nonnegative by SUPINF_2:58;
then Q5: Integral M,(max- f) = integral+ M,(max- f) by Q0, MESFUNC5:94;
for x being Element of X st x in dom (max- f) holds
0 = (max- f) . x

proof

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 AS, Q1, Q2a, PARTFUN1:34;
hence 0 = (max- f) . x by MESFUNC2:21; :: thesis: verum

end;

then Integral M,(max- f) = 0 by Q0, LPSPACE1:22;
hence f is_integrable_on M by AS, Q2, Q4, Q5, MESFUNC5:def 17; :: thesis: verum

end;

hence ( Integral M,f in REAL iff f is_integrable_on M ) by H1; :: thesis: verum