let A be non empty closed_interval Subset of REAL; :: thesis:
let f, g be PartFunc of REAL,REAL; :: thesis:
let X be open Subset of REAL; :: thesis:
assume that
A1: f is_differentiable_on X and
A2: g is_differentiable_on X and
A3: A c= X and
A4: f `| X is_integrable_on A and
A5: (f `| X) | A is bounded and
A6: g `| X is_integrable_on A and
A7: (g `| X) | A is bounded ; :: thesis:
A8: (f (#) g) `| X = ((f `| X) (#) g) + (f (#) (g `| X)) by A1, A2, FDIFF_2:20;
g | X is continuous by A2, FDIFF_1:25;
then A9: g | A is continuous by A3, FCONT_1:16;
X c= dom g by A2, FDIFF_1:def 6;
then A10: A c= dom g by A3, XBOOLE_1:1;
then A11: g || A is Function of A,REAL by Th6, FUNCT_2:68;
X c= dom g by A2, FDIFF_1:def 6;
then g is_integrable_on A by A3, A9, Th11, XBOOLE_1:1;
then A12: g || A is integrable ;
A13: A c= dom (g `| X) by A2, A3, FDIFF_1:def 7;
then A14: (g `| X) || A is Function of A,REAL by Th6, FUNCT_2:68;
g | X is continuous by A2, FDIFF_1:25;
then g | A is bounded by A3, A10, Th10, FCONT_1:16;
then A15: ((f `| X) (#) g) | (A /\ A) is bounded by A5, RFUNCT_1:84;
then A16: (((f `| X) (#) g) || A) | A is bounded ;
f | X is continuous by A1, FDIFF_1:25;
then A17: f | A is continuous by A3, FCONT_1:16;
X c= dom f by A1, FDIFF_1:def 6;
then f is_integrable_on A by A3, A17, Th11, XBOOLE_1:1;
then A18: f || A is integrable ;
A19: A c= dom (f `| X) by A1, A3, FDIFF_1:def 7;
then A20: (f `| X) || A is Function of A,REAL by Th6, FUNCT_2:68;
A21: ( (g `| X) || A is integrable & ((g `| X) || A) | A is bounded ) by A6, A7;
A22: ( (f `| X) || A is integrable & ((f `| X) || A) | A is bounded ) by A4, A5;
dom ((f `| X) (#) g) = (dom (f `| X)) /\ (dom g) by VALUED_1:def 4;
then A c= dom ((f `| X) (#) g) by A10, A19, XBOOLE_1:19;
then A23: ((f `| X) (#) g) || A is Function of A,REAL by Th6, FUNCT_2:68;
X c= dom f by A1, FDIFF_1:def 6;
then A24: A c= dom f by A3, XBOOLE_1:1;
then A25: f || A is Function of A,REAL by Th6, FUNCT_2:68;
f | X is continuous by A1, FDIFF_1:25;
then f | A is bounded by A3, A24, Th10, FCONT_1:16;
then A26: (f (#) (g `| X)) | (A /\ A) is bounded by A7, RFUNCT_1:84;
then A27: ((f (#) (g `| X)) || A) | A is bounded ;
(((f `| X) (#) g) + (f (#) (g `| X))) | (A /\ A) is bounded by A15, A26, RFUNCT_1:83;
then A28: ((f (#) g) `| X) | A is bounded by A1, A2, FDIFF_2:20;
A29: ( (f (#) g) . (upper_bound A) = (f . (upper_bound A)) * (g . (upper_bound A)) & (f (#) g) . (lower_bound A) = (f . (lower_bound A)) * (g . (lower_bound A)) ) by VALUED_1:5;
dom (f (#) (g `| X)) = (dom f) /\ (dom (g `| X)) by VALUED_1:def 4;
then A c= dom (f (#) (g `| X)) by A24, A13, XBOOLE_1:19;
then A30: (f (#) (g `| X)) || A is Function of A,REAL by Th6, FUNCT_2:68;
(g || A) | A is bounded by A9, A10, Th10;
then ((f `| X) || A) (#) (g || A) is integrable by A12, A11, A20, A22, INTEGRA4:29;
then A31: ((f `| X) (#) g) || A is integrable by Th4;
(f || A) | A is bounded by A17, A24, Th10;
then (f || A) (#) ((g `| X) || A) is integrable by A18, A25, A14, A21, INTEGRA4:29;
then A32: (f (#) (g `| X)) || A is integrable by Th4;
then integral ((((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A)) = (integral (((f `| X) (#) g) || A)) + (integral ((f (#) (g `| X)) || A)) by A31, A23, A16, A30, A27, INTEGRA1:57;
then A33: integral ((((f `| X) (#) g) + (f (#) (g `| X))) || A) = (integral (((f `| X) (#) g),A)) + (integral ((f (#) (g `| X)),A)) by Th5;
(((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A) is integrable by A31, A32, A23, A16, A30, A27, INTEGRA1:57;
then (((f `| X) (#) g) + (f (#) (g `| X))) || A is integrable by Th5;
then A34: (f (#) g) `| X is_integrable_on A by A8;
integral (((f (#) g) `| X) || A) = integral (((f (#) g) `| X),A)
.= ((f (#) g) . (upper_bound A)) - ((f (#) g) . (lower_bound A)) by A1, A2, A3, A34, A28, Th13, FDIFF_2:20 ;
hence integral (((f `| X) (#) g),A) = (((f . (upper_bound A)) * (g . (upper_bound A))) - ((f . (lower_bound A)) * (g . (lower_bound A)))) - (integral ((f (#) (g `| X)),A)) by A8, A29, A33; :: thesis: