let X be non empty set ; 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; 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; 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; 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; 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; ( f is_integrable_on M implies Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) )
assume
f is_integrable_on M
; 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;
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; verum