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 E -measurable & g is E -measurable holds

f (#) g is E -measurable

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 E -measurable & g is E -measurable holds

f (#) g is E -measurable

let E be Element of S; :: thesis: for f, g being PartFunc of X,REAL 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,REAL; :: 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 & g is E -measurable ) ; :: thesis: f (#) g is E -measurable

( R_EAL f is E -measurable & R_EAL g is E -measurable ) by A2, MESFUNC6:def 1;

then (R_EAL f) (#) (R_EAL g) is E -measurable by A1, MESFUNC7:15;

then R_EAL (f (#) g) is E -measurable by Th30;

hence f (#) g is E -measurable by MESFUNC6:def 1; :: thesis: verum

for E being Element of S

for f, g being PartFunc of X,REAL 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 E being Element of S

for f, g being PartFunc of X,REAL 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: for f, g being PartFunc of X,REAL 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,REAL; :: 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 & g is E -measurable ) ; :: thesis: f (#) g is E -measurable

( R_EAL f is E -measurable & R_EAL g is E -measurable ) by A2, MESFUNC6:def 1;

then (R_EAL f) (#) (R_EAL g) is E -measurable by A1, MESFUNC7:15;

then R_EAL (f (#) g) is E -measurable by Th30;

hence f (#) g is E -measurable by MESFUNC6:def 1; :: thesis: verum