theorem :: INTEGR26:45

for f being PartFunc of REAL,REAL
for a being Real
for I being non empty Interval st f is_differentiable_on_interval I & a in I holds
integral ((f `\ I),a,a) = 0