theorem Th66: :: INTEGRA8:66

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))