theorem Th67: :: INTEGRA8:67

for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded holds
integral (((f `| Z) - (g `| Z)),A) = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A)))