theorem :: INTEGR26:48

for a, b being 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))