let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,COMPLEX
for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,COMPLEX
for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let f, g be PartFunc of X,COMPLEX ; :: thesis: for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds
f (#) g is_measurable_on E
let E be Element of S; :: thesis: ( (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E )
assume A1: ( (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E ) ; :: thesis: f (#) g is_measurable_on E
then A2: ( Re f is_measurable_on E & Im f is_measurable_on E & Re g is_measurable_on E & Im g is_measurable_on E ) by MESFUN6C:def 3;
A3: ( dom (Re f) = dom f & dom (Im f) = dom f & dom (Re g) = dom g & dom (Im g) = dom g ) by MESFUN6C:def 1, MESFUN6C:def 2;
then A4: ( (Re f) (#) (Re g) is_measurable_on E & (Re f) (#) (Im g) is_measurable_on E & (Im f) (#) (Re g) is_measurable_on E & (Im f) (#) (Im g) is_measurable_on E ) by A1, A2, MES715;
dom ((Im f) (#) (Im g)) = E by A3, A1, VALUED_1:def 4;
then ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) is_measurable_on E by A4, MESFUNC6:29;
then A5: Re (f (#) g) is_measurable_on E by COM715;
((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) is_measurable_on E by A4, MESFUNC6:26;
then Im (f (#) g) is_measurable_on E by COM715;
hence f (#) g is_measurable_on E by A5, MESFUN6C:def 3; :: thesis: verum