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
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
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
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
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; :: 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:61;
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:61;

A4: now :: thesis: for x being object st x in dom ((c (#) f) | B) holds
((c (#) f) | B) . x = (c (#) (f | B)) . x

let x be object ; :: 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:47;
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:47;
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:2;
hence Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) by A1, Th40; :: thesis: verum