theorem :: INTEGRA7:33

for f, P being PartFunc of REAL,REAL
for x, y, a, b, s, t being Real st x <= y & s <= t & ['s,t'] c= ].a,b.[ & ['x,y'] c= dom f & f is continuous & P is_differentiable_on ].a,b.[ & P .: ].a,b.[ is open Subset of REAL & P `| ].a,b.[ is continuous & P .: ].a,b.[ c= ].x,y.[ & ['s,t'] c= dom (f * P) holds
( f | ['x,y'] is bounded & f is_integrable_on ['x,y'] & ((f * P) (#) (P `| ].a,b.[)) | ['s,t'] is continuous & ['s,t'] c= dom ((f * P) (#) (P `| ].a,b.[)) & ((f * P) (#) (P `| ].a,b.[)) | ['s,t'] is bounded & (f * P) (#) (P `| ].a,b.[) is_integrable_on ['s,t'] & integral (((f * P) (#) (P `| ].a,b.[)),s,t) = integral (f,(P . s),(P . t)) )