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 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 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 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 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 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 ; :: thesis: ( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )
set d = - c;
A3: (- c) (#) (- f) = (- c) (#) ((- 1) (#) f) by MESFUNC2:9
.= ((- c) * (- 1)) (#) f by Th35 ;
hence Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) by A2, A1, Th30, Th59; :: thesis: Integral (M,(c (#) f)) = - (c * (integral' (M,(- f))))
Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) by A2, A1, A3, Th30, Th59;
hence Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) by XXREAL_3:92; :: thesis: verum