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