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 ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
Integral M,f = integral+ M,f
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
Integral M,f = integral+ M,f
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative holds
Integral M,f = integral+ M,f
let f be PartFunc of X,ExtREAL ; :: thesis: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative implies Integral M,f = integral+ M,f )
assume that
A1: ex A being Element of S st
( A = dom f & f is_measurable_on A ) and
A2: f is nonnegative ; :: thesis: Integral M,f = integral+ M,f
A3: dom f = dom (max+ f) by MESFUNC2:def 2;

A4: now

let x be set ; :: thesis: ( x in dom f implies (max+ f) . x = f . x )
A5: 0 <= f . x by A2, SUPINF_2:70;
assume x in dom f ; :: thesis: (max+ f) . x = f . x
hence (max+ f) . x = max (f . x),0 by A3, MESFUNC2:def 2
.= f . x by A5, XXREAL_0:def 10 ;
:: thesis: verum

end;

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

A7: now

let x be Element of X; :: thesis: ( x in dom (max- f) implies (max- f) . x = 0 )
assume x in dom (max- f) ; :: thesis: (max- f) . x = 0
then (max+ f) . x = f . x by A4, A6;
hence (max- f) . x = 0 by MESFUNC2:21; :: thesis: verum

end;

A8: dom f = dom (max- f) by MESFUNC2:def 3;
f = max+ f by A3, A4, FUNCT_1:9;
hence Integral M,f = (integral+ M,f) - (R_EAL 0 ) by A1, A7, A8, Th93, MESFUNC2:28
.= integral+ M,f by XXREAL_3:15 ;
:: thesis: verum