let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
for c being Complex
for A being Element of S st f is A -measurable & A c= dom f holds
c (#) f is A -measurable

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX
for c being Complex
for A being Element of S st f is A -measurable & A c= dom f holds
c (#) f is A -measurable

let f be PartFunc of X,COMPLEX; :: thesis: for c being Complex
for A being Element of S st f is A -measurable & A c= dom f holds
c (#) f is A -measurable

let c be Complex; :: thesis: for A being Element of S st f is A -measurable & A c= dom f holds
c (#) f is A -measurable

let A be Element of S; :: thesis: ( f is A -measurable & A c= dom f implies c (#) f is A -measurable )
assume that
A1: f is A -measurable and
A2: A c= dom f ; :: thesis: c (#) f is A -measurable
A3: dom (Im f) = dom f by COMSEQ_3:def 4;
A4: Im f is A -measurable by A1;
then A5: (Re c) (#) (Im f) is A -measurable by ;
A6: (Im c) (#) (Im f) is A -measurable by ;
A7: dom (Re f) = dom f by COMSEQ_3:def 3;
A8: Re f is A -measurable by A1;
then (Im c) (#) (Re f) is A -measurable by ;
then ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) is A -measurable by ;
then A9: Im (c (#) f) is A -measurable 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 ;
(Re c) (#) (Re f) is A -measurable by ;
then ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) is A -measurable by ;
then Re (c (#) f) is A -measurable by Th3;
hence c (#) f is A -measurable by A9; :: thesis: verum