theorem :: INTEGRA5:18

for f being PartFunc of REAL,REAL
for A, B, C being non empty closed_interval Subset of REAL
for X being set st A c= X & f is_differentiable_on X & (f `| X) | A is continuous & lower_bound A = lower_bound B & upper_bound B = lower_bound C & upper_bound C = upper_bound A holds
( B c= A & C c= A & integral ((f `| X),A) = (integral ((f `| X),B)) + (integral ((f `| X),C)) )