let A be closed-interval Subset of REAL ; :: thesis: for f, g being PartFunc of REAL ,REAL st A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded holds
f (#) g is_integrable_on A
let f, g be PartFunc of REAL ,REAL ; :: thesis: ( A c= dom f & A c= dom g & f is_integrable_on A & f | A is bounded & g is_integrable_on A & g | A is bounded implies f (#) g is_integrable_on A )
assume that
A1: ( A c= dom f & A c= dom g ) and
A2: ( f is_integrable_on A & f | A is bounded ) and
A3: ( g is_integrable_on A & g | A is bounded ) ; :: thesis: f (#) g is_integrable_on A
A4: ( f || A is integrable & (f || A) | A is bounded ) by A2, INTEGRA5:9, INTEGRA5:def 2;
A5: ( g || A is integrable & (g || A) | A is bounded ) by A3, INTEGRA5:9, INTEGRA5:def 2;
A6: (f || A) (#) (g || A) = (f (#) g) || A by INTEGRA5:4;
( f || A is Function of A,REAL & g || A is Function of A,REAL ) by A1, Lm1;
then (f (#) g) || A is integrable by A4, A5, A6, INTEGRA4:29;
hence f (#) g is_integrable_on A by INTEGRA5:def 2; :: thesis: verum