theorem :: INTEGR11:30

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