let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX st ex A being Element of S st dom f = A holds
for c being Complex
for B being Element of S st f is B -measurable holds
c (#) f is B -measurable
let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st dom f = A holds
for c being Complex
for B being Element of S st f is B -measurable holds
c (#) f is B -measurable
let f be PartFunc of X,COMPLEX; :: thesis: ( ex A being Element of S st dom f = A implies for c being Complex
for B being Element of S st f is B -measurable holds
c (#) f is B -measurable )
assume ex A being Element of S st A = dom f ; :: thesis: for c being Complex
for B being Element of S st f is B -measurable holds
c (#) f is B -measurable
then consider A being Element of S such that
A1: A = dom f ;

hereby :: thesis: verum

let c be Complex; :: thesis: for B being Element of S st f is B -measurable holds
c (#) f is B -measurable
let B be Element of S; :: thesis: ( f is B -measurable implies c (#) f is B -measurable )
A2: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5;
A3: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5;
dom (Re (c (#) f)) = dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) by Th3;
then A4: dom (Re (c (#) f)) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f))) by VALUED_1:12;
A5: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def 5;
dom (Im (c (#) f)) = dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) by Th3;
then A6: dom (Im (c (#) f)) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f))) by VALUED_1:def 1;
A7: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def 5;
A8: dom (Re f) = dom f by COMSEQ_3:def 3;
A9: dom (Im f) = dom f by COMSEQ_3:def 4;
assume A10: f is B -measurable ; :: thesis: c (#) f is B -measurable
then Im f is B -measurable ;
then A11: Im f is A /\ B -measurable by A1, A9, MESFUNC6:80;
Re f is B -measurable by A10;
then Re f is A /\ B -measurable by A1, A8, MESFUNC6:80;
then f is A /\ B -measurable by A11;
then A12: c (#) f is A /\ B -measurable by A1, Th17, XBOOLE_1:17;
then Im (c (#) f) is A /\ B -measurable ;
then A13: Im (c (#) f) is B -measurable by A1, A8, A9, A5, A7, A6, MESFUNC6:80;
Re (c (#) f) is A /\ B -measurable by A12;
then Re (c (#) f) is B -measurable by A1, A8, A9, A2, A3, A4, MESFUNC6:80;
hence c (#) f is B -measurable by A13; :: thesis: verum

end;