let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X, COMPLEX
for c being complex number
for A being Element of S st f is_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A
let S be SigmaField of X; :: thesis: for f being PartFunc of X, COMPLEX
for c being complex number
for A being Element of S st f is_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A
let f be PartFunc of X, COMPLEX ; :: thesis: for c being complex number
for A being Element of S st f is_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A
let c be complex number ; :: thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds
c (#) f is_measurable_on A
let A be Element of S; :: thesis: ( f is_measurable_on A & A c= dom f implies c (#) f is_measurable_on A )
assume A1: ( f is_measurable_on A & A c= dom f ) ; :: thesis: c (#) f is_measurable_on A
then A2: ( Re f is_measurable_on A & Im f is_measurable_on A ) by Def3;
( dom (Re f) = dom f & dom (Im f) = dom f ) by Def1, Def2;
then A4: ( (Re c) (#) (Re f) is_measurable_on A & (Im c) (#) (Re f) is_measurable_on A & (Re c) (#) (Im f) is_measurable_on A & (Im c) (#) (Im f) is_measurable_on A ) by A1, A2, MESFUNC6:21;
then ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) is_measurable_on A by MESFUNC6:26;
then A5: Im (c (#) f) is_measurable_on A by COM21;
dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5;
then A c= dom ((Im c) (#) (Im f)) by A1, Def2;
then ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) is_measurable_on A by A4, MESFUNC6:29;
then Re (c (#) f) is_measurable_on A by COM21;
hence c (#) f is_measurable_on A by A5, Def3; :: thesis: verum