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

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