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 & f is_measurable_on B holds
( f | B is_integrable_on M & Integral_on M,B,(c (#) f) = (R_EAL 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 & f is_measurable_on B holds
( f | B is_integrable_on M & Integral_on M,B,(c (#) f) = (R_EAL 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 & f is_measurable_on B holds
( f | B is_integrable_on M & Integral_on M,B,(c (#) f) = (R_EAL 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 & f is_measurable_on B holds
( f | B is_integrable_on M & Integral_on M,B,(c (#) f) = (R_EAL c) * (Integral_on M,B,f) )
let c be Real; :: thesis: for B being Element of S st f is_integrable_on M & f is_measurable_on B holds
( f | B is_integrable_on M & Integral_on M,B,(c (#) f) = (R_EAL c) * (Integral_on M,B,f) )
let B be Element of S; :: thesis: ( f is_integrable_on M & f is_measurable_on B implies ( f | B is_integrable_on M & Integral_on M,B,(c (#) f) = (R_EAL c) * (Integral_on M,B,f) ) )
assume A1: ( f is_integrable_on M & f is_measurable_on B ) ; :: thesis: ( f | B is_integrable_on M & Integral_on M,B,(c (#) f) = (R_EAL c) * (Integral_on M,B,f) )
A2: f | B is_integrable_on M by A1, Th103;
dom ((c (#) f) | B) = (dom (c (#) f)) /\ B by RELAT_1:90;
then dom ((c (#) f) | B) = (dom f) /\ B by MESFUNC1:def 6;
then dom ((c (#) f) | B) = dom (f | B) by RELAT_1:90;
then A3: dom ((c (#) f) | B) = dom (c (#) (f | B)) by MESFUNC1:def 6;
for x being set st x in dom ((c (#) f) | B) holds
((c (#) f) | B) . x = (c (#) (f | B)) . x

proof

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 x in (dom (c (#) f)) /\ B by RELAT_1:90;
then A5: ( x in (dom f) /\ B & x in dom (c (#) f) ) by MESFUNC1:def 6, XBOOLE_0:def 4;
then A6: x in dom (f | B) by RELAT_1:90;
then A7: x in dom (c (#) (f | B)) by MESFUNC1:def 6;
((c (#) f) | B) . x = (c (#) f) . x by A4, FUNCT_1:70;
then ((c (#) f) | B) . x = (R_EAL c) * (f . x) by A5, MESFUNC1:def 6;
then ((c (#) f) | B) . x = (R_EAL c) * ((f | B) . x) by A6, FUNCT_1:70;
hence ((c (#) f) | B) . x = (c (#) (f | B)) . x by A7, MESFUNC1:def 6; :: thesis: verum

end;

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