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 that
A1: (dom f) /\ (dom g) = E and
A2: f is_measurable_on E and
A3: g is_measurable_on E ; :: thesis: f (#) g is_measurable_on E
A4: dom (Im g) = dom g by COMSEQ_3:def 4;
A5: Im f is_measurable_on E by A2, MESFUN6C:def 1;
A6: dom (Im f) = dom f by COMSEQ_3:def 4;
then A7: dom ((Im f) (#) (Im g)) = E by A1, A4, VALUED_1:def 4;
A8: Im g is_measurable_on E by A3, MESFUN6C:def 1;
then A9: (Im f) (#) (Im g) is_measurable_on E by A1, A5, A6, A4, Th31;
A10: dom (Re f) = dom f by COMSEQ_3:def 3;
A11: dom (Re g) = dom g by COMSEQ_3:def 3;
A12: Re g is_measurable_on E by A3, MESFUN6C:def 1;
then A13: (Im f) (#) (Re g) is_measurable_on E by A1, A5, A6, A11, Th31;
A14: Re f is_measurable_on E by A2, MESFUN6C:def 1;
then (Re f) (#) (Im g) is_measurable_on E by A1, A8, A10, A4, Th31;
then ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) is_measurable_on E by A13, MESFUNC6:26;
then A15: Im (f (#) g) is_measurable_on E by Th32;
(Re f) (#) (Re g) is_measurable_on E by A1, A14, A12, A10, A11, Th31;
then ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) is_measurable_on E by A9, A7, MESFUNC6:29;
then Re (f (#) g) is_measurable_on E by Th32;
hence f (#) g is_measurable_on E by A15, MESFUN6C:def 1; :: thesis: verum