let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being nonpositive PartFunc of X,ExtREAL st f is_simple_func_in S holds
( Integral (M,f) = - (integral' (M,(- f))) & Integral (M,f) = - (integral' (M,(max- f))) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being nonpositive PartFunc of X,ExtREAL st f is_simple_func_in S holds
( Integral (M,f) = - (integral' (M,(- f))) & Integral (M,f) = - (integral' (M,(max- f))) )

let M be sigma_Measure of S; :: thesis: for f being nonpositive PartFunc of X,ExtREAL st f is_simple_func_in S holds
( Integral (M,f) = - (integral' (M,(- f))) & Integral (M,f) = - (integral' (M,(max- f))) )

let f be nonpositive PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S implies ( Integral (M,f) = - (integral' (M,(- f))) & Integral (M,f) = - (integral' (M,(max- f))) ) )
assume A1: f is_simple_func_in S ; :: thesis: ( Integral (M,f) = - (integral' (M,(- f))) & Integral (M,f) = - (integral' (M,(max- f))) )
then reconsider A = dom f as Element of S by MESFUNC5:37;
A2: f is A -measurable by ;
integral+ (M,(- f)) = integral' (M,(- f)) by ;
hence A3: Integral (M,f) = - (integral' (M,(- f))) by ; :: thesis: Integral (M,f) = - (integral' (M,(max- f)))
f = - (max- f) by Th32;
hence Integral (M,f) = - (integral' (M,(max- f))) by ; :: thesis: verum