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 & f is_measurable_on B 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 & f is_measurable_on B 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 & f is_measurable_on B 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 & f is_measurable_on B 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 & f is_measurable_on B 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 & f is_measurable_on B implies Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f) )
assume ( f is_integrable_on M & f is_measurable_on B ) ; :: thesis: Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f)
then A2: f | B is_integrable_on M by Th91;
B0: 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 B1: dom ((c (#) f) | B) = dom (f | B) by RELAT_1:90;
then A3: dom ((c (#) f) | B) = dom (c (#) (f | B)) by VALUED_1:def 5;

now

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

end;

then (c (#) f) | B = c (#) (f | B) by A3, FUNCT_1:9;
hence Integral_on M,B,(c (#) f) = c * (Integral_on M,B,f) by A2, Th102; :: thesis: verum