let A be non empty closed_interval Subset of REAL; :: thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds
f (#) g is integrable
let f, g be Function of A,REAL; :: thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable implies f (#) g is integrable )
assume that
A1: f | A is bounded and
A2: f is integrable and
A3: g | A is bounded and
A4: g is integrable ; :: thesis: f (#) g is integrable
A5: (f (#) g) | (A /\ A) is bounded by A1, A3, RFUNCT_1:84;
consider r2 being real number such that
A6: for x being set st x in A /\ (dom g) holds
abs (g . x) <= r2 by A3, RFUNCT_1:73;
A7: A /\ (dom g) = A /\ A by FUNCT_2:def 1
.= A ;
A8: A /\ (dom f) = A /\ A by FUNCT_2:def 1
.= A ;
then consider a being Element of REAL such that
A9: a in A /\ (dom f) by SUBSET_1:4;
reconsider a = a as Element of A by A9;
A10: abs (f . a) >= 0 by COMPLEX1:46;
consider r1 being real number such that
A11: for x being set st x in A /\ (dom f) holds
abs (f . x) <= r1 by A1, RFUNCT_1:73;
reconsider r = max (r1,r2) as Real by XREAL_0:def 1;
A12: r2 <= r by XXREAL_0:25;
A13: r1 <= r by XXREAL_0:25;
A14: for x, y being Real st x in A & y in A holds
abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y))))

proof

let x, y be Real; :: thesis: ( x in A & y in A implies abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) )
assume that
A15: x in A and
A16: y in A ; :: thesis: abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y))))
A17: (f (#) g) . y = (f . y) * (g . y) by VALUED_1:5;
abs (g . y) <= r2 by A6, A7, A16;
then A18: abs (g . y) <= r by A12, XXREAL_0:2;
A19: abs ((f . x) - (f . y)) >= 0 by COMPLEX1:46;
abs (((f . x) - (f . y)) * (g . y)) = (abs ((f . x) - (f . y))) * (abs (g . y)) by COMPLEX1:65;
then A20: abs (((f . x) - (f . y)) * (g . y)) <= r * (abs ((f . x) - (f . y))) by A19, A18, XREAL_1:64;
(f (#) g) . x = (f . x) * (g . x) by VALUED_1:5;
then abs (((f (#) g) . x) - ((f (#) g) . y)) = abs (((f . x) * ((g . x) - (g . y))) + (((f . x) - (f . y)) * (g . y))) by A17;
then A21: abs (((f (#) g) . x) - ((f (#) g) . y)) <= (abs ((f . x) * ((g . x) - (g . y)))) + (abs (((f . x) - (f . y)) * (g . y))) by COMPLEX1:56;
abs (f . x) <= r1 by A11, A8, A15;
then A22: abs (f . x) <= r by A13, XXREAL_0:2;
A23: abs ((g . x) - (g . y)) >= 0 by COMPLEX1:46;
abs ((f . x) * ((g . x) - (g . y))) = (abs (f . x)) * (abs ((g . x) - (g . y))) by COMPLEX1:65;
then abs ((f . x) * ((g . x) - (g . y))) <= r * (abs ((g . x) - (g . y))) by A23, A22, XREAL_1:64;
then (abs ((f . x) * ((g . x) - (g . y)))) + (abs (((f . x) - (f . y)) * (g . y))) <= (r * (abs ((g . x) - (g . y)))) + (r * (abs ((f . x) - (f . y)))) by A20, XREAL_1:7;
hence abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) by A21, XXREAL_0:2; :: thesis: verum

end;

A24: abs (f . a) <= r1 by A11, A9;

now

per cases ( r = 0 or r > 0 ) by A24, A10, XXREAL_0:25;

suppose A25: r = 0 ; :: thesis: f (#) g is integrable

for x, y being Real st x in A & y in A holds
abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y)))

proof

let x, y be Real; :: thesis: ( x in A & y in A implies abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y))) )
assume that
A26: x in A and
A27: y in A ; :: thesis: abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y)))
abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) by A14, A26, A27;
hence abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y))) by A25, COMPLEX1:46; :: thesis: verum

end;

hence f (#) g is integrable by A1, A2, A5, Th27; :: thesis: verum

end;

suppose r > 0 ; :: thesis: f (#) g is integrable

hence f (#) g is integrable by A1, A2, A3, A4, A5, A14, Th28; :: thesis: verum

end;

end;

end;

hence f (#) g is integrable ; :: thesis: verum