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 st ex A being Element of S st dom f = A holds
for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex A being Element of S st dom f = A holds
for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st ex A being Element of S st dom f = A holds
for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let f be PartFunc of X,ExtREAL ; :: thesis: ( ex A being Element of S st dom f = A implies for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B )
assume A1: ex A being Element of S st A = dom f ; :: thesis: for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let c be Real; :: thesis: for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let B be Element of S; :: thesis: ( f is_measurable_on B implies c (#) f is_measurable_on B )
assume A2: f is_measurable_on B ; :: thesis: c (#) f is_measurable_on B
consider A being Element of S such that
A3: A = dom f by A1;
f is_measurable_on A /\ B by A2, A3, Th54;
then A4: c (#) f is_measurable_on A /\ B by A3, MESFUNC1:41, XBOOLE_1:17;
dom (c (#) f) = A by A3, MESFUNC1:def 6;
hence c (#) f is_measurable_on B by A4, Th54; :: thesis: verum