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 A1: ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & f is nonnegative ) ; :: thesis: Integral M,f = integral+ M,f
then consider A being Element of S such that
A2: ( A = dom f & f is_measurable_on A ) ;
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 )
assume A5: x in dom f ; :: thesis: (max+ f) . x = f . x
A6: 0 <= f . x by A1, SUPINF_2:70;
thus (max+ f) . x = max (f . x),0 by A3, A5, MESFUNC2:def 2
.= f . x by A6, XXREAL_0:def 10 ; :: thesis: verum

end;

then A7: f = max+ f by A3, FUNCT_1:9;
A8: dom f = dom (max- f) by MESFUNC2:def 3;

A9: 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, A8;
hence (max- f) . x = 0 by MESFUNC2:21; :: thesis: verum

end;

dom f = dom (max- f) by MESFUNC2:def 3;
hence Integral M,f = (integral+ M,f) - (R_EAL 0 ) by A2, A7, A9, Th93, MESFUNC2:28
.= integral+ M,f by XXREAL_3:15 ;
:: thesis: verum