let A be 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
consider r1 being real number such that
A5: for x being set st x in A /\ (dom f) holds
abs (f . x) <= r1 by A1, RFUNCT_1:90;
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:90;
reconsider r = max r1,r2 as Real by XREAL_0:def 1;
A7: ( f (#) g is total & (f (#) g) | A is bounded )

proof

thus f (#) g is total ; :: thesis: (f (#) g) | A is bounded
(f (#) g) | (A /\ A) is bounded by A1, A3, RFUNCT_1:101;
hence (f (#) g) | A is bounded ; :: thesis: verum

end;

A8: ( r1 <= r & r2 <= r ) by XXREAL_0:25;
A9: A /\ (dom f) = A /\ A by FUNCT_2:def 1
.= A ;
then consider a being Element of REAL such that
A10: a in A /\ (dom f) by SUBSET_1:10;
reconsider a = a as Element of A by A10;
A11: ( abs (f . a) <= r1 & abs (f . a) >= 0 ) by A5, A10, COMPLEX1:132;
A12: A /\ (dom g) = A /\ A by FUNCT_2:def 1
.= A ;
A13: 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 A14: ( x in A & y in A ) ; :: thesis: abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y))))
( (f (#) g) . x = (f . x) * (g . x) & (f (#) g) . y = (f . y) * (g . y) ) 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))) ;
then A15: abs (((f (#) g) . x) - ((f (#) g) . y)) <= (abs ((f . x) * ((g . x) - (g . y)))) + (abs (((f . x) - (f . y)) * (g . y))) by COMPLEX1:142;
A16: abs ((f . x) * ((g . x) - (g . y))) = (abs (f . x)) * (abs ((g . x) - (g . y))) by COMPLEX1:151;
A17: abs ((g . x) - (g . y)) >= 0 by COMPLEX1:132;
abs (f . x) <= r1 by A5, A9, A14;
then abs (f . x) <= r by A8, XXREAL_0:2;
then A18: abs ((f . x) * ((g . x) - (g . y))) <= r * (abs ((g . x) - (g . y))) by A16, A17, XREAL_1:66;
A19: abs (((f . x) - (f . y)) * (g . y)) = (abs ((f . x) - (f . y))) * (abs (g . y)) by COMPLEX1:151;
A20: abs ((f . x) - (f . y)) >= 0 by COMPLEX1:132;
abs (g . y) <= r2 by A6, A12, A14;
then abs (g . y) <= r by A8, XXREAL_0:2;
then abs (((f . x) - (f . y)) * (g . y)) <= r * (abs ((f . x) - (f . y))) by A19, A20, XREAL_1:66;
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 A18, XREAL_1:9;
hence abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) by A15, XXREAL_0:2; :: thesis: verum

end;

now

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

suppose A21: 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 ( x in A & y in A ) ; :: thesis: abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y)))
then abs (((f (#) g) . x) - ((f (#) g) . y)) <= r * ((abs ((g . x) - (g . y))) + (abs ((f . x) - (f . y)))) by A13;
hence abs (((f (#) g) . x) - ((f (#) g) . y)) <= 1 * (abs ((f . x) - (f . y))) by A21, COMPLEX1:132; :: thesis: verum

end;

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

end;

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

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

end;

end;

end;

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