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 that
A1: f is_measurable_on A and
A2: A c= dom f ; :: thesis: c (#) f is_measurable_on A
A3: dom (Im f) = dom f by COMSEQ_3:def 4;
A4: Im f is_measurable_on A by A1, Def3;
then A5: (Re c) (#) (Im f) is_measurable_on A by A2, A3, MESFUNC6:21;
A6: (Im c) (#) (Im f) is_measurable_on A by A2, A4, A3, MESFUNC6:21;
A7: dom (Re f) = dom f by COMSEQ_3:def 3;
A8: Re f is_measurable_on A by A1, Def3;
then (Im c) (#) (Re f) is_measurable_on A by A2, A7, MESFUNC6:21;
then ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) is_measurable_on A by A5, MESFUNC6:26;
then A9: Im (c (#) f) is_measurable_on A by Th3;
dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5;
then A10: A c= dom ((Im c) (#) (Im f)) by A2, COMSEQ_3:def 4;
(Re c) (#) (Re f) is_measurable_on A by A2, A8, A7, MESFUNC6:21;
then ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) is_measurable_on A by A6, A10, MESFUNC6:29;
then Re (c (#) f) is_measurable_on A by Th3;
hence c (#) f is_measurable_on A by A9, Def3; :: thesis: verum