theorem Th57: :: INTEGRA8:57
for A being non empty closed_interval Subset of REAL holds integral (cosh,A) = (sinh . (upper_bound A)) - (sinh . (lower_bound A))