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
for c being Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds
( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds
( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds
( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )

let f be PartFunc of X,ExtREAL; :: thesis: for c being Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds
( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )

let c be Real; :: thesis: ( f is_simple_func_in S & f is nonpositive & 0 <= c implies ( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) ) )
assume that
A1: f is_simple_func_in S and
A2: f is nonpositive and
A3: 0 <= c ; :: thesis: ( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )
A4: c (#) f is_simple_func_in S by ;
f = - (max- f) by ;
then A6: - f = max- f by Th36;
A7: - f is_simple_func_in S by ;
A8: max- (c (#) f) = c (#) (max- f) by ;
c (#) f is nonpositive by A2, A3, Th4;
hence Integral (M,(c (#) f)) = - (integral' (M,(max- (c (#) f)))) by
.= - (c * (integral' (M,(- f)))) by ;
:: thesis: Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f)))
hence Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) by XXREAL_3:92; :: thesis: verum