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 E -measurable & g is E -measurable holds
f (#) g is E -measurable
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 E -measurable & g is E -measurable holds
f (#) g is E -measurable
let f, g be PartFunc of X,COMPLEX; :: thesis: for E being Element of S st (dom f) /\ (dom g) = E & f is E -measurable & g is E -measurable holds
f (#) g is E -measurable
let E be Element of S; :: thesis: ( (dom f) /\ (dom g) = E & f is E -measurable & g is E -measurable implies f (#) g is E -measurable )
assume that
A1: (dom f) /\ (dom g) = E and
A2: f is E -measurable and
A3: g is E -measurable ; :: thesis: f (#) g is E -measurable
A4: dom (Im g) = dom g by COMSEQ_3:def 4;
A5: Im f is E -measurable 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 E -measurable by A3, MESFUN6C:def 1;
then A9: (Im f) (#) (Im g) is E -measurable 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 E -measurable by A3, MESFUN6C:def 1;
then A13: (Im f) (#) (Re g) is E -measurable by A1, A5, A6, A11, Th31;
A14: Re f is E -measurable by A2, MESFUN6C:def 1;
then (Re f) (#) (Im g) is E -measurable by A1, A8, A10, A4, Th31;
then ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) is E -measurable by A13, MESFUNC6:26;
then A15: Im (f (#) g) is E -measurable by Th32;
(Re f) (#) (Re g) is E -measurable by A1, A14, A12, A10, A11, Th31;
then ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) is E -measurable by A9, A7, MESFUNC6:29;
then Re (f (#) g) is E -measurable by Th32;
hence f (#) g is E -measurable by A15, MESFUN6C:def 1; :: thesis: verum