let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for f, g being PartFunc of X,REAL 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 E being Element of S
for f, g being PartFunc of X,REAL 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: for f, g being PartFunc of X,REAL 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,REAL; :: 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 & g is_measurable_on E ) ; :: thesis: f (#) g is_measurable_on E
( R_EAL f is_measurable_on E & R_EAL g is_measurable_on E ) by A2, MESFUNC6:def 1;
then (R_EAL f) (#) (R_EAL g) is_measurable_on E by A1, MESFUNC7:15;
then R_EAL (f (#) g) is_measurable_on E by Th30;
hence f (#) g is_measurable_on E by MESFUNC6:def 1; :: thesis: verum