let a, b be Real; :: 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'] and
A4: g is_integrable_on ['b,a'] and
A5: f | ['b,a'] is bounded and
A6: 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)) )
set I = ['b,a'];
assume that
A7: X c= dom f and
A8: X c= dom g and
A9: F is_integral_of f,X and
A10: 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))
A11: X c= dom G by A10, Th11;
then A12: ['b,a'] c= dom G by A2;
A13: G is_differentiable_on X by A10, Lm1;
then A14: G | X is continuous by FDIFF_1:25;
then A15: G | ['b,a'] is bounded by A2, A12, FCONT_1:16, INTEGRA5:10;
then A16: (f (#) G) | (['b,a'] /\ ['b,a']) is bounded by A5, RFUNCT_1:84;
A17: X c= dom F by A9, Th11;
then A18: ['b,a'] c= dom F by A2;
A19: F is_differentiable_on X by A9, Lm1;
then A20: X is open Subset of REAL by FDIFF_1:8, FDIFF_1:10;
A21: F | X is continuous by A19, FDIFF_1:25;
then A22: F | ['b,a'] is bounded by A2, A18, FCONT_1:16, INTEGRA5:10;
then A23: (F (#) g) | (['b,a'] /\ ['b,a']) is bounded by A6, RFUNCT_1:84;
then A24: ((f (#) G) + (F (#) g)) | (['b,a'] /\ ['b,a']) is bounded by A16, RFUNCT_1:83;
F | ['b,a'] is continuous by A2, A21, FCONT_1:16;
then A25: F is_integrable_on ['b,a'] by A18, INTEGRA5:17;
['b,a'] c= dom g by A2, A8;
then A26: F (#) g is_integrable_on ['b,a'] by A4, A6, A18, A25, A22, INTEGRA6:14;
( F `| X = f | X & G `| X = g | X ) by A9, A10, Lm1;
then (F (#) G) `| X = ((f | X) (#) G) + (F (#) (g | X)) by A19, A13, A20, FDIFF_2:20;
then (F (#) G) `| X = ((f (#) G) | X) + (F (#) (g | X)) by RFUNCT_1:45;
then (F (#) G) `| X = ((f (#) G) | X) + ((F (#) g) | X) by RFUNCT_1:45;
then A27: (F (#) G) `| X = ((f (#) G) + (F (#) g)) | X by RFUNCT_1:44;
F (#) G is_differentiable_on X by A19, A13, A20, FDIFF_2:20;
then A28: F (#) G is_integral_of (f (#) G) + (F (#) g),X by A27, Lm1;
min (b,a) = b by A1, XXREAL_0:def 9;
then A29: max (b,a) = a by XXREAL_0:36;
( b <= max (b,a) & [.b,a.] = ['b,a'] ) by A1, INTEGRA5:def 3, XXREAL_0:25;
then A30: ( b in ['b,a'] & a in ['b,a'] ) by A29;
X c= (dom F) /\ (dom g) by A8, A17, XBOOLE_1:19;
then X c= dom (F (#) g) by VALUED_1:def 4;
then A31: ['b,a'] c= dom (F (#) g) by A2;
G | ['b,a'] is continuous by A2, A14, FCONT_1:16;
then A32: G is_integrable_on ['b,a'] by A12, INTEGRA5:17;
X c= (dom f) /\ (dom G) by A7, A11, XBOOLE_1:19;
then X c= dom (f (#) G) by VALUED_1:def 4;
then A33: ['b,a'] c= dom (f (#) G) by A2;
['b,a'] c= dom f by A2, A7;
then A34: f (#) G is_integrable_on ['b,a'] by A3, A5, A12, A32, A15, INTEGRA6:14;
then (f (#) G) + (F (#) g) is_integrable_on ['b,a'] by A33, A31, A26, A16, A23, INTEGRA6:11;
then (F (#) G) . a = (integral (((f (#) G) + (F (#) g)),b,a)) + ((F (#) G) . b) by A1, A2, A24, A28, Th18;
then ( (F (#) G) . b = (F . b) * (G . b) & ((F (#) G) . a) - ((F (#) G) . b) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) ) by A1, A33, A31, A34, A26, A16, A23, A30, INTEGRA6:24, VALUED_1:5;
hence ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) by VALUED_1:5; :: thesis: verum