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,COMPLEX
for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f)
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX
for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f)
let f be PartFunc of X,COMPLEX ; :: thesis: for c being complex number
for B being Element of S st f is_integrable_on M holds
Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f)
let c be complex number ; :: thesis: for B being Element of S st f is_integrable_on M holds
Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f)
let B be Element of S; :: thesis: ( f is_integrable_on M implies Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f) )
assume f is_integrable_on M ; :: thesis: Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f)
then A1: f | B is_integrable_on M by Th23;
A2: dom ((c (#) f) | B) = (dom (c (#) f)) /\ B by RELAT_1:90;
then dom ((c (#) f) | B) = (dom f) /\ B by VALUED_1:def 5;
then A3: dom ((c (#) f) | B) = dom (f | B) by RELAT_1:90;

A4: now

let x be set ; :: thesis: ( x in dom ((c (#) f) | B) implies ((c (#) f) | B) . x = (c (#) (f | B)) . x )
assume A5: x in dom ((c (#) f) | B) ; :: thesis: ((c (#) f) | B) . x = (c (#) (f | B)) . x
then A6: ((c (#) f) | B) . x = (c (#) f) . x by FUNCT_1:70;
x in dom (c (#) f) by A2, A5, XBOOLE_0:def 4;
then ((c (#) f) | B) . x = c * (f . x) by A6, VALUED_1:def 5;
then A7: ((c (#) f) | B) . x = c * ((f | B) . x) by A3, A5, FUNCT_1:70;
x in dom (c (#) (f | B)) by A3, A5, VALUED_1:def 5;
hence ((c (#) f) | B) . x = (c (#) (f | B)) . x by A7, VALUED_1:def 5; :: thesis: verum

end;

dom ((c (#) f) | B) = dom (c (#) (f | B)) by A3, VALUED_1:def 5;
then (c (#) f) | B = c (#) (f | B) by A4, FUNCT_1:9;
hence Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f) by A1, Th40; :: thesis: verum