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 A1, MESFUNC2:34;

integral+ (M,(- f)) = integral' (M,(- f)) by A1, Th30, MESFUNC5:77;

hence A3: Integral (M,f) = - (integral' (M,(- f))) by A2, Th57; :: thesis: Integral (M,f) = - (integral' (M,(max- f)))

f = - (max- f) by Th32;

hence Integral (M,f) = - (integral' (M,(max- f))) by A3, Th36; :: thesis: verum

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 A1, MESFUNC2:34;

integral+ (M,(- f)) = integral' (M,(- f)) by A1, Th30, MESFUNC5:77;

hence A3: Integral (M,f) = - (integral' (M,(- f))) by A2, Th57; :: thesis: Integral (M,f) = - (integral' (M,(max- f)))

f = - (max- f) by Th32;

hence Integral (M,f) = - (integral' (M,(max- f))) by A3, Th36; :: thesis: verum