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 such that
A6: for x being object st x in A /\ (dom g) holds
|.(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: |.(f . a).| >= 0 by COMPLEX1:46;
consider r1 being Real such that
A11: for x being object st x in A /\ (dom f) holds
|.(f . x).| <= r1 by A1, RFUNCT_1:73;
reconsider r = max (r1,r2) as Real ;
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
|.(((f (#) g) . x) - ((f (#) g) . y)).| <= r * (|.((g . x) - (g . y)).| + |.((f . x) - (f . y)).|)

proof

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

end;

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

now :: thesis: f (#) g is integrable

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
|.(((f (#) g) . x) - ((f (#) g) . y)).| <= 1 * |.((f . x) - (f . y)).|

proof

let x, y be Real; :: thesis: ( x in A & y in A implies |.(((f (#) g) . x) - ((f (#) g) . y)).| <= 1 * |.((f . x) - (f . y)).| )
assume that
A26: x in A and
A27: y in A ; :: thesis: |.(((f (#) g) . x) - ((f (#) g) . y)).| <= 1 * |.((f . x) - (f . y)).|
|.(((f (#) g) . x) - ((f (#) g) . y)).| <= r * (|.((g . x) - (g . y)).| + |.((f . x) - (f . y)).|) by A14, A26, A27;
hence |.(((f (#) g) . x) - ((f (#) g) . y)).| <= 1 * |.((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