let X be non empty set ; 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; 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; 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; 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; ( 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
; 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; verum