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 & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & 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 & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & 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 & X c= dom f & X c= dom g & f | X is continuous & g | X is continuous & 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 ; :: thesis: ( not X c= dom f or not X c= dom g or not f | X is continuous or not g | X is continuous 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
A3: X c= dom f and
A4: X c= dom g and
A5: f | X is continuous and
A6: g | X is continuous and
A7: ( 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))
A8: [.b,a.] c= dom f by A2, A3;
A9: [.b,a.] = ['b,a'] by A1, INTEGRA5:def 3;
then f | ['b,a'] is continuous by A2, A5, FCONT_1:16;
then A10: f is_integrable_on ['b,a'] by A8, A9, INTEGRA5:17;
A11: [.b,a.] c= dom g by A2, A4;
then A12: g | ['b,a'] is bounded by A2, A6, A9, FCONT_1:16, INTEGRA5:10;
g | ['b,a'] is continuous by A2, A6, A9, FCONT_1:16;
then A13: g is_integrable_on ['b,a'] by A11, A9, INTEGRA5:17;
f | ['b,a'] is bounded by A2, A5, A8, A9, FCONT_1:16, INTEGRA5:10;
hence ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral ((f (#) G),b,a)) + (integral ((F (#) g),b,a)) by A1, A2, A3, A4, A7, A9, A10, A13, A12, Th21; :: thesis: verum