theorem :: INTEGR11:31

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