let A be non empty 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;

A5: ( g || A is integrable & (g || A) | A is bounded ) by A3;

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 ; :: thesis: verum

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;

A5: ( g || A is integrable & (g || A) | A is bounded ) by A3;

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 ; :: thesis: verum