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 A2, A3, MESFUNC6:21;
A6: (Im c) (#) (Im f) is A -measurable by A2, A4, A3, MESFUNC6:21;
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 A2, A7, MESFUNC6:21;
then ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) is A -measurable by A5, MESFUNC6:26;
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 A2, COMSEQ_3:def 4;
(Re c) (#) (Re f) is A -measurable by A2, A8, A7, MESFUNC6:21;
then ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) is A -measurable by A6, A10, MESFUNC6:29;
then Re (c (#) f) is A -measurable by Th3;
hence c (#) f is A -measurable by A9; :: thesis: verum