theorem :: INTEGRA8:98

for A being non empty closed_interval Subset of REAL holds integral ((sinh (#) sinh),A) = (((cosh . (upper_bound A)) * (sinh . (upper_bound A))) - ((cosh . (lower_bound A)) * (sinh . (lower_bound A)))) - (integral ((cosh (#) cosh),A))