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
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & 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,ExtREAL
for c being Real
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & 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,ExtREAL
for c being Real
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) )
let f be PartFunc of X,ExtREAL; :: thesis: for c being Real
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) )
let c be Real; :: thesis: for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M & 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 ( f | B is_integrable_on M & Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) ) )
assume f is_integrable_on M ; :: thesis: ( f | B 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 Th97;
A2: for x being object st x in dom ((c (#) f) | B) holds
((c (#) f) | B) . x = (c (#) (f | B)) . x

proof

let x be object ; :: thesis: ( x in dom ((c (#) f) | B) implies ((c (#) f) | B) . x = (c (#) (f | B)) . x )
assume A3: x in dom ((c (#) f) | B) ; :: thesis: ((c (#) f) | B) . x = (c (#) (f | B)) . x
then A4: ((c (#) f) | B) . x = (c (#) f) . x by FUNCT_1:47;
A5: x in (dom (c (#) f)) /\ B by A3, RELAT_1:61;
then x in (dom f) /\ B by MESFUNC1:def 6;
then A6: x in dom (f | B) by RELAT_1:61;
x in dom (c (#) f) by A5, XBOOLE_0:def 4;
then ((c (#) f) | B) . x = c * (f . x) by A4, MESFUNC1:def 6;
then A7: ((c (#) f) | B) . x = c * ((f | B) . x) by A6, FUNCT_1:47;
x in dom (c (#) (f | B)) by A6, MESFUNC1:def 6;
hence ((c (#) f) | B) . x = (c (#) (f | B)) . x by A7, MESFUNC1:def 6; :: thesis: verum

end;

dom ((c (#) f) | B) = (dom (c (#) f)) /\ B by RELAT_1:61;
then dom ((c (#) f) | B) = (dom f) /\ B by MESFUNC1:def 6;
then dom ((c (#) f) | B) = dom (f | B) by RELAT_1:61;
then dom ((c (#) f) | B) = dom (c (#) (f | B)) by MESFUNC1:def 6;
then (c (#) f) | B = c (#) (f | B) by A2, FUNCT_1:2;
hence ( f | B is_integrable_on M & Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) ) by A1, Th110; :: thesis: verum