let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let S be SigmaField of X; :: thesis: for f being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let f be PartFunc of X,REAL; :: thesis: for A being Element of S
for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let A be Element of S; :: thesis: for r being Real st f is_measurable_on A & A c= dom f holds
r (#) f is_measurable_on A
let r be Real; :: thesis: ( f is_measurable_on A & A c= dom f implies r (#) f is_measurable_on A )
assume that
A1: f is_measurable_on A and
A2: A c= dom f ; :: thesis: r (#) f is_measurable_on A
R_EAL f is_measurable_on A by A1;
then r (#) (R_EAL f) is_measurable_on A by A2, MESFUNC1:37;
then R_EAL (r (#) f) is_measurable_on A by Th20;
hence r (#) f is_measurable_on A ; :: thesis: verum