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 A -measurable ) & 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 A -measurable ) & 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 A -measurable ) & 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 A -measurable ) & 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 A -measurable ) and
A2: f is nonnegative ; :: thesis: Integral (M,f) = integral+ (M,f)
A3: dom f = dom (max+ f) by MESFUNC2:def 2;

A4: now :: thesis: for x being object st x in dom f holds
(max+ f) . x = f . x

let x be object ; :: thesis: ( x in dom f implies (max+ f) . x = f . x )
A5: 0 <= f . x by A2, SUPINF_2:51;
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 :: thesis: for x being Element of X st x in dom (max- f) holds
(max- f) . x = 0

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:19; :: thesis: verum

end;

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