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 A1, MESFUNC5:39;
f = - (max- f) by A2, Th32;
then A6: - f = max- f by Th36;
A7: - f is_simple_func_in S by A1, Th30;
A8: max- (c (#) f) = c (#) (max- f) by A3, MESFUNC5:26;
c (#) f is nonpositive by A2, A3, Th4;
hence Integral (M,(c (#) f)) = - (integral' (M,(max- (c (#) f)))) by A4, Th58
.= - (c * (integral' (M,(- f)))) by A3, A7, A6, A8, Th5, MESFUNC5:66 ;
:: thesis: Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f)))
hence Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) by XXREAL_3:92; :: thesis: verum