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

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