let A be 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 is_differentiable_on X & (f (#) g) `| X = ((f `| X) (#) g) + (f (#) (g `| X)) ) by A1, A2, FDIFF_2:20;
X c= dom f by A1, FDIFF_1:def 7;
then Xf: A c= dom f by A3, XBOOLE_1:1;
X c= dom g by A2, FDIFF_1:def 7;
then Xg: A c= dom g by A3, XBOOLE_1:1;
A9: ( f | X is continuous & g | X is continuous ) by A1, A2, FDIFF_1:33;
( f | X is continuous & g | X is continuous ) by A1, A2, FDIFF_1:33;
then A10: ( f | A is continuous & g | A is continuous ) by A3, FCONT_1:17;
then ( f is_integrable_on A & g is_integrable_on A ) by Th11, Xf, Xg;
then A11: ( f || A is integrable & g || A is integrable & (f `| X) || A is integrable & (g `| X) || A is integrable ) by A4, A6, Def2;
( X c= dom f & X c= dom g ) by A1, A2, FDIFF_1:def 7;
then A12: ( A c= dom f & A c= dom g ) by A3, XBOOLE_1:1;
then A13: ( f || A is Function of A,REAL & g || A is Function of A,REAL ) by Th6, FUNCT_2:131;
( f | A is continuous & g | A is continuous ) by A3, A9, FCONT_1:17;
then A14: ( f | A is bounded & g | A is bounded ) by Th10, A12;
A15: ( (f || A) | A is bounded & (g || A) | A is bounded ) by A10, Th9, Th10, A12;
A16: ( A c= dom (f `| X) & A c= dom (g `| X) ) by A1, A2, A3, FDIFF_1:def 8;
then A17: ( (f `| X) || A is Function of A,REAL & (g `| X) || A is Function of A,REAL ) by Th6, FUNCT_2:131;
( ((f `| X) || A) | A is bounded & ((g `| X) || A) | A is bounded ) by A5, A7, Th9;
then ( ((f `| X) || A) (#) (g || A) is integrable & (f || A) (#) ((g `| X) || A) is integrable ) by A11, A13, A15, A17, INTEGRA4:29;
then A18: ( ((f `| X) (#) g) || A is integrable & (f (#) (g `| X)) || A is integrable ) by Th4;
dom ((f `| X) (#) g) = (dom (f `| X)) /\ (dom g) by VALUED_1:def 4;
then A c= dom ((f `| X) (#) g) by A12, A16, XBOOLE_1:19;
then A19: ((f `| X) (#) g) || A is Function of A,REAL by Th6, FUNCT_2:131;
A20: ((f `| X) (#) g) | (A /\ A) is bounded by A5, A14, RFUNCT_1:101;
then A21: (((f `| X) (#) g) || A) | A is bounded by Th9;
dom (f (#) (g `| X)) = (dom f) /\ (dom (g `| X)) by VALUED_1:def 4;
then A c= dom (f (#) (g `| X)) by A12, A16, XBOOLE_1:19;
then A22: (f (#) (g `| X)) || A is Function of A,REAL by Th6, FUNCT_2:131;
A23: (f (#) (g `| X)) | (A /\ A) is bounded by A7, A14, RFUNCT_1:101;
then A24: ((f (#) (g `| X)) || A) | A is bounded by Th9;
A25: f (#) g is_differentiable_on X by A1, A2, FDIFF_2:20;
A26: (f (#) g) `| X is_integrable_on A

proof

(((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A) is integrable by A18, A19, A21, A22, A24, INTEGRA1:59;
then (((f `| X) (#) g) + (f (#) (g `| X))) || A is integrable by Th5;
hence (f (#) g) `| X is_integrable_on A by A8, Def2; :: thesis:

end;

A27: ((f (#) g) `| X) | A is bounded

proof

(((f `| X) (#) g) + (f (#) (g `| X))) | (A /\ A) is bounded by A20, A23, RFUNCT_1:100;
hence ((f (#) g) `| X) | A is bounded by A1, A2, FDIFF_2:20; :: thesis:

end;

A28: integral (((f (#) g) `| X) || A) = integral ((f (#) g) `| X),A
.= ((f (#) g) . (sup A)) - ((f (#) g) . (inf A)) by A3, A25, A26, A27, Th13 ;
A29: ( (f (#) g) . (sup A) = (f . (sup A)) * (g . (sup A)) & (f (#) g) . (inf A) = (f . (inf A)) * (g . (inf A)) ) by VALUED_1:5;
integral ((((f `| X) (#) g) || A) + ((f (#) (g `| X)) || A)) = (integral (((f `| X) (#) g) || A)) + (integral ((f (#) (g `| X)) || A)) by A18, A19, A21, A22, A24, INTEGRA1:59;
then integral ((((f `| X) (#) g) + (f (#) (g `| X))) || A) = (integral ((f `| X) (#) g),A) + (integral (f (#) (g `| X)),A) by Th5;
hence integral ((f `| X) (#) g),A = (((f . (sup A)) * (g . (sup A))) - ((f . (inf A)) * (g . (inf A)))) - (integral (f (#) (g `| X)),A) by A8, A28, A29; :: thesis: