let A be non empty closed_interval Subset of REAL; for f, g being PartFunc of REAL,REAL
for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds
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))
let f, g be PartFunc of REAL,REAL; for X being open Subset of REAL st f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded holds
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))
let X be open Subset of REAL; ( f is_differentiable_on X & g is_differentiable_on X & A c= X & f `| X is_integrable_on A & (f `| X) | A is bounded & g `| X is_integrable_on A & (g `| X) | A is bounded implies 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)) )
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
; 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))
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; verum