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 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 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 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 holds
Integral (M,(c (#) f)) = c * (integral' (M,f))
let c be Real; :: thesis: ( f is_simple_func_in S & f is nonnegative implies Integral (M,(c (#) f)) = c * (integral' (M,f)) )
assume that
A1: f is_simple_func_in S and
a2: f is nonnegative ; :: thesis: Integral (M,(c (#) f)) = c * (integral' (M,f))
per cases ( c >= 0 or c < 0 ) ;
suppose A2: c >= 0 ; :: thesis: Integral (M,(c (#) f)) = c * (integral' (M,f))
then A3: ( c (#) f is_simple_func_in S & c (#) f is nonnegative ) by A1, a2, MESFUNC5:20, MESFUNC5:39;
integral' (M,(c (#) f)) = c * (integral' (M,f)) by A1, a2, A2, MESFUNC5:66;
hence Integral (M,(c (#) f)) = c * (integral' (M,f)) by A3, MESFUNC5:89; :: thesis: verum
end;
suppose c < 0 ; :: thesis: Integral (M,(c (#) f)) = c * (integral' (M,f))
hence Integral (M,(c (#) f)) = c * (integral' (M,f)) by A1, a2, Lm4; :: thesis: verum
end;
end;