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
A3: 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 )
assume f is_measurable_on B ; :: thesis: c (#) f is_measurable_on B
then B1: ( Re f is_measurable_on B & Im f is_measurable_on B ) by Def3;
C1: ( dom (Re f) = dom f & dom (Im f) = dom f ) by Def1, Def2;
then ( Re f is_measurable_on A /\ B & Im f is_measurable_on A /\ B ) by A3, B1, MESFUNC6:80;
then f is_measurable_on A /\ B by Def3;
then c (#) f is_measurable_on A /\ B by A3, Th21, XBOOLE_1:17;
then B3: ( Re (c (#) f) is_measurable_on A /\ B & Im (c (#) f) is_measurable_on A /\ B ) by Def3;
D1: ( dom ((Re c) (#) (Re f)) = dom (Re f) & dom ((Im c) (#) (Im f)) = dom (Im f) & dom ((Im c) (#) (Re f)) = dom (Re f) & dom ((Re c) (#) (Im f)) = dom (Im f) ) by VALUED_1:def 5;
( dom (Re (c (#) f)) = dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) & dom (Im (c (#) f)) = dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) ) by COM21;
then ( dom (Re (c (#) f)) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f))) & dom (Im (c (#) f)) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f))) ) by VALUED_1:12, VALUED_1:def 1;
then ( Re (c (#) f) is_measurable_on B & Im (c (#) f) is_measurable_on B ) by C1, D1, A3, B3, MESFUNC6:80;
hence c (#) f is_measurable_on B by Def3; :: thesis: verum

end;