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 & 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 & X c= dom g ) and
A4: ( f | X is continuous & g | X is continuous ) and
A5: ( 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)
X: ( [.b,a.] c= dom f & [.b,a.] c= dom g ) by A2, A3, XBOOLE_1:1;
A6: [.b,a.] = ['b,a'] by A1, INTEGRA5:def 4;
then ( f | ['b,a'] is continuous & g | ['b,a'] is continuous ) by A2, A4, FCONT_1:17;
then ( f is_integrable_on ['b,a'] & f | ['b,a'] is bounded & g is_integrable_on ['b,a'] & g | ['b,a'] is bounded ) by X, A6, INTEGRA5:10, INTEGRA5:17;
hence ((F . a) * (G . a)) - ((F . b) * (G . b)) = (integral (f (#) G),b,a) + (integral (F (#) g),b,a) by A1, A2, A3, A5, A6, Th21; :: thesis: verum