let b, a be real number ; :: thesis: for X being set
for f, g, F, G being PartFunc of REAL , REAL st b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X holds
((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral (f (#) G),b,a) + (integral (F (#) g),b,a)
let X be set ; :: thesis: for f, g, F, G being PartFunc of REAL , REAL st b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X holds
((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral (f (#) G),b,a) + (integral (F (#) g),b,a)
let f, g, F, G be PartFunc of REAL , REAL ; :: thesis: ( b <= a & ['b,a'] c= X & f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g | ['b,a'] is bounded & X c= dom f & X c= dom g & F is_integral_of f,X & G is_integral_of g,X implies ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral (f (#) G),b,a) + (integral (F (#) g),b,a) )
assume that
A1: b <= a and
A2: ['b,a'] c= X and
A3: ( f is_integrable_on ['b,a'] & g is_integrable_on ['b,a'] ) and
A4: ( f | ['b,a'] is bounded & g | ['b,a'] is bounded ) ; :: thesis: ( not X c= dom f or not X c= dom g or not F is_integral_of f,X or not G is_integral_of g,X or ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral (f (#) G),b,a) + (integral (F (#) g),b,a) )
assume that
A5: ( X c= dom f & X c= dom g ) and
A6: ( F is_integral_of f,X & G is_integral_of g,X ) ; :: thesis: ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral (f (#) G),b,a) + (integral (F (#) g),b,a)
set I = ['b,a'];
A7: ( X c= dom F & X c= dom G ) by A6, Th11;
then ( X c= (dom f) /\ (dom G) & X c= (dom F) /\ (dom g) ) by A5, XBOOLE_1:19;
then ( X c= dom (f (#) G) & X c= dom (F (#) g) ) by VALUED_1:def 4;
then A8: ( ['b,a'] c= dom (f (#) G) & ['b,a'] c= dom (F (#) g) ) by A2, XBOOLE_1:1;
A9: ( F is_differentiable_on X & F `| X = f | X & G is_differentiable_on X & G `| X = g | X ) by A6, Lm1;
then A10: X is open Subset of REAL by FDIFF_1:15, FDIFF_1:17;
then A11: F (#) G is_differentiable_on X by A9, FDIFF_2:20;
( F | X is continuous & G | X is continuous ) by A9, FDIFF_1:33;
then Y: ( F | ['b,a'] is continuous & G | ['b,a'] is continuous ) by A2, FCONT_1:17;
X: ( ['b,a'] c= dom f & ['b,a'] c= dom g & ['b,a'] c= dom F & ['b,a'] c= dom G ) by A2, A5, A7, XBOOLE_1:1;
then A12: ( F is_integrable_on ['b,a'] & G is_integrable_on ['b,a'] & F | ['b,a'] is bounded & G | ['b,a'] is bounded ) by Y, INTEGRA5:10, INTEGRA5:17;
A13: ( f (#) G is_integrable_on ['b,a'] & F (#) g is_integrable_on ['b,a'] & (f (#) G) | (['b,a'] /\ ['b,a']) is bounded & (F (#) g) | (['b,a'] /\ ['b,a']) is bounded ) by A3, A4, A12, X, INTEGRA6:14, RFUNCT_1:101;
then A14: ( (f (#) G) + (F (#) g) is_integrable_on ['b,a'] & ((f (#) G) + (F (#) g)) | (['b,a'] /\ ['b,a']) is bounded ) by A8, INTEGRA6:11, RFUNCT_1:100;
A15: ( min b,a <= b & b <= max b,a ) by XXREAL_0:17, XXREAL_0:25;
A16: [.b,a.] = ['b,a'] by A1, INTEGRA5:def 4;
min b,a = b by A1, XXREAL_0:def 9;
then max b,a = a by XXREAL_0:36;
then A17: ( b in ['b,a'] & a in ['b,a'] ) by A15, A16, XXREAL_1:1;
A18: (F (#) G) . b = (F . b) * (G . b) by VALUED_1:5;
(F (#) G) `| X = ((f | X) (#) G) + (F (#) (g | X)) by A9, A10, FDIFF_2:20;
then (F (#) G) `| X = ((f (#) G) | X) + (F (#) (g | X)) by RFUNCT_1:61;
then (F (#) G) `| X = ((f (#) G) | X) + ((F (#) g) | X) by RFUNCT_1:61;
then (F (#) G) `| X = ((f (#) G) + (F (#) g)) | X by RFUNCT_1:60;
then F (#) G is_integral_of (f (#) G) + (F (#) g),X by A11, Lm1;
then (F (#) G) . a = (integral ((f (#) G) + (F (#) g)),b,a) + ((F (#) G) . b) by A1, A2, A14, Th18;
then ((F (#) G) . a) - ((F (#) G) . b) = (integral (f (#) G),b,a) + (integral (F (#) g),b,a) by A1, A8, A13, A17, INTEGRA6:24;
hence ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral (f (#) G),b,a) + (integral (F (#) g),b,a) by A18, VALUED_1:5; :: thesis: verum