let A be 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 ( 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