theorem :: INTEGRA8:58

for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds
integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e)