theorem :: INTEGR26:47

for a, b, p, q being Real
for f, g being PartFunc of REAL,REAL st a < b & p < q & [.a,b.] c= dom f & f | ['a,b'] is continuous & g is_differentiable_on_interval ['p,q'] & g `\ ['p,q'] is_integrable_on ['p,q'] & g `\ ['p,q'] is bounded & rng (g | ['p,q']) c= ['a,b'] & g . p = a & g . q = b holds
integral (f,a,b) = integral (((f * g) (#) (g `\ ['p,q'])),p,q)