let a, b be Real; for f, g being PartFunc of REAL,REAL st a < b & f is_differentiable_on_interval ['a,b'] & g is_differentiable_on_interval ['a,b'] & f `\ ['a,b'] is_integrable_on ['a,b'] & f `\ ['a,b'] is bounded & g `\ ['a,b'] is_integrable_on ['a,b'] & g `\ ['a,b'] is bounded holds
integral (((f `\ ['a,b']) (#) g),a,b) = (((f . b) * (g . b)) - ((f . a) * (g . a))) - (integral ((f (#) (g `\ ['a,b'])),a,b))
let f, g be PartFunc of REAL,REAL; ( a < b & f is_differentiable_on_interval ['a,b'] & g is_differentiable_on_interval ['a,b'] & f `\ ['a,b'] is_integrable_on ['a,b'] & f `\ ['a,b'] is bounded & g `\ ['a,b'] is_integrable_on ['a,b'] & g `\ ['a,b'] is bounded implies integral (((f `\ ['a,b']) (#) g),a,b) = (((f . b) * (g . b)) - ((f . a) * (g . a))) - (integral ((f (#) (g `\ ['a,b'])),a,b)) )
assume that
A1:
a < b
and
A2:
f is_differentiable_on_interval ['a,b']
and
A3:
g is_differentiable_on_interval ['a,b']
and
A4:
f `\ ['a,b'] is_integrable_on ['a,b']
and
A5:
f `\ ['a,b'] is bounded
and
A6:
g `\ ['a,b'] is_integrable_on ['a,b']
and
A7:
g `\ ['a,b'] is bounded
; integral (((f `\ ['a,b']) (#) g),a,b) = (((f . b) * (g . b)) - ((f . a) * (g . a))) - (integral ((f (#) (g `\ ['a,b'])),a,b))
reconsider I = ['a,b'] as non empty closed_interval Subset of REAL ;
f (#) g is_differentiable_on_interval I
by A2, A3, FDIFF_12:24;
then A8:
dom ((f (#) g) `\ I) = I
by FDIFF_12:def 2;
A9:
(f (#) g) `\ I = ((f `\ I) (#) g) + (f (#) (g `\ I))
by A2, A3, FDIFF_12:24;
A10:
( I c= dom f & I c= dom g )
by A2, A3, FDIFF_12:def 1;
then A11:
( f || I is Function of I,REAL & g || I is Function of I,REAL )
by INTEGRA5:6, FUNCT_2:68;
A12:
( f is_integrable_on I & g is_integrable_on I )
by A10, A2, A3, FDIFF_12:37, INTEGRA5:11;
A13:
( I = dom (f `\ I) & I = dom (g `\ I) )
by A2, A3, FDIFF_12:def 2;
then A14:
( (f `\ I) || I is Function of I,REAL & (g `\ I) || I is Function of I,REAL )
by INTEGRA5:6, FUNCT_2:68;
A15:
( (f `\ I) | I is bounded & (g `\ I) | I is bounded )
by A5, A7;
( f | I is bounded & g | I is bounded )
by A2, A10, A3, FDIFF_12:37, INTEGRA5:10;
then A16:
( (f (#) (g `\ I)) | (I /\ I) is bounded & ((f `\ I) (#) g) | (I /\ I) is bounded )
by A15, RFUNCT_1:84;
then A17:
( ((f (#) (g `\ I)) || I) | I is bounded & (((f `\ I) (#) g) || I) | I is bounded )
;
A18:
( (g `\ I) || I is integrable & ((g `\ I) || I) | I is bounded )
by A6, A7;
A19:
( (f `\ I) || I is integrable & ((f `\ I) || I) | I is bounded )
by A4, A5;
( dom ((f `\ I) (#) g) = (dom (f `\ I)) /\ (dom g) & dom (f (#) (g `\ I)) = (dom f) /\ (dom (g `\ I)) )
by VALUED_1:def 4;
then
( I = dom ((f `\ I) (#) g) & I = dom (f (#) (g `\ I)) )
by A10, A13, XBOOLE_1:28;
then A20:
( ((f `\ I) (#) g) || I is Function of I,REAL & (f (#) (g `\ I)) || I is Function of I,REAL )
by INTEGRA5:6, FUNCT_2:68;
(((f `\ I) (#) g) + (f (#) (g `\ I))) | (I /\ I) is bounded
by A16, RFUNCT_1:83;
then A21:
((f (#) g) `\ I) | I is bounded
by A2, A3, FDIFF_12:24;
A22:
( (f (#) g) . b = (f . b) * (g . b) & (f (#) g) . a = (f . a) * (g . a) )
by VALUED_1:5;
( (f || I) | I is bounded & (g || I) | I is bounded )
by A2, A10, A3, FDIFF_12:37, INTEGRA5:10;
then
( (f || I) (#) ((g `\ I) || I) is integrable & ((f `\ I) || I) (#) (g || I) is integrable )
by A14, A18, A12, A11, A19, INTEGRA4:29;
then
( (f (#) (g `\ I)) || I is integrable & ((f `\ I) (#) g) || I is integrable )
by INTEGRA5:4;
then
( (((f `\ I) (#) g) || I) + ((f (#) (g `\ I)) || I) is integrable & integral ((((f `\ I) (#) g) || I) + ((f (#) (g `\ I)) || I)) = (integral (((f `\ I) (#) g) || I)) + (integral ((f (#) (g `\ I)) || I)) )
by A20, A17, INTEGRA1:57;
then A23:
( (f (#) g) `\ I is_integrable_on I & integral ((((f `\ I) (#) g) + (f (#) (g `\ I))) || I) = (integral (((f `\ I) (#) g),I)) + (integral ((f (#) (g `\ I)),I)) )
by A9, INTEGRA5:5;
then
integral (((f (#) g) `\ I),I) = ((f (#) g) . b) - ((f (#) g) . a)
by A1, A2, A3, A8, A21, Lm4, FDIFF_12:24;
then
integral (((f `\ ['a,b']) (#) g),a,b) = (((f . b) * (g . b)) - ((f . a) * (g . a))) - (integral ((f (#) (g `\ ['a,b'])),I))
by A1, A9, A22, A23, INTEGRA5:def 4;
hence
integral (((f `\ ['a,b']) (#) g),a,b) = (((f . b) * (g . b)) - ((f . a) * (g . a))) - (integral ((f (#) (g `\ ['a,b'])),a,b))
by A1, INTEGRA5:def 4; verum