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 nonnegative & c <= 0 holds
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 nonnegative & c <= 0 holds
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 nonnegative & c <= 0 holds
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 nonnegative & c <= 0 holds
Integral (M,(c (#) f)) = c * (integral' (M,f))
let c be Real; :: thesis: ( f is_simple_func_in S & f is nonnegative & c <= 0 implies Integral (M,(c (#) f)) = c * (integral' (M,f)) )
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative and
A3: c <= 0 ; :: thesis: Integral (M,(c (#) f)) = c * (integral' (M,f))
set d = - c;
A4: - f is_simple_func_in S by A1, Th30;
(- c) (#) (- f) = (- c) (#) ((- 1) (#) f) by MESFUNC2:9
.= ((- c) * (- 1)) (#) f by Th35 ;
then Integral (M,(c (#) f)) = (- (- c)) * (integral' (M,(- (- f)))) by A3, A2, A4, Lm3;
hence Integral (M,(c (#) f)) = c * (integral' (M,f)) by DBLSEQ_3:2; :: thesis: verum