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 number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
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 number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let f be PartFunc of X,COMPLEX ; :: thesis: ( ex A being Element of S st dom f = A implies for c being complex number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B )
assume ex A being Element of S st A = dom f ; :: thesis: for c being complex number
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
then consider A being Element of S such that
A1: A = dom f ;

hereby :: thesis: verum

let c be complex number ; :: thesis: for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
let B be Element of S; :: thesis: ( f is_measurable_on B implies c (#) f is_measurable_on B )
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_measurable_on B ; :: thesis: c (#) f is_measurable_on B
then Im f is_measurable_on B by Def3;
then A11: Im f is_measurable_on A /\ B by A1, A9, MESFUNC6:80;
Re f is_measurable_on B by A10, Def3;
then Re f is_measurable_on A /\ B by A1, A8, MESFUNC6:80;
then f is_measurable_on A /\ B by A11, Def3;
then A12: c (#) f is_measurable_on A /\ B by A1, Th17, XBOOLE_1:17;
then Im (c (#) f) is_measurable_on A /\ B by Def3;
then A13: Im (c (#) f) is_measurable_on B by A1, A8, A9, A5, A7, A6, MESFUNC6:80;
Re (c (#) f) is_measurable_on A /\ B by A12, Def3;
then Re (c (#) f) is_measurable_on B by A1, A8, A9, A2, A3, A4, MESFUNC6:80;
hence c (#) f is_measurable_on B by A13, Def3; :: thesis: verum

end;