let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,1.] implies integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e) )
assume A = [.0,1.] ; :: thesis: integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e)
then A = [.0,jj.] ;
then ( upper_bound A = 1 & lower_bound A = 0 ) by Th37;
then integral (cosh,A) = (sinh . 1) - 0 by Th57, SIN_COS2:16
.= ((number_e ^2) - 1) / (2 * number_e) by Th17 ;
hence integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e) ; :: thesis: verum