theorem Th78: :: INTEGRA8:78

for A being non empty closed_interval Subset of REAL holds integral ((sin - cos),A) = (((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) - ((sin . (upper_bound A)) - (sin . (lower_bound A)))