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 A1: ( 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 ) ; :: thesis: f (#) g is_integrable_on A
then A2: ( f || A is integrable & (f || A) | A is bounded & g || A is integrable & (g || A) | A is bounded ) by INTEGRA5:9, INTEGRA5:def 2;
A3: ( f || A is Function of A,REAL & g || A is Function of A,REAL ) by A1, Lm1;
(f || A) (#) (g || A) = (f (#) g) || A by INTEGRA5:4;
then (f (#) g) || A is integrable by A2, A3, INTEGRA4:29;
hence f (#) g is_integrable_on A by INTEGRA5:def 2; :: thesis: verum