let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,1.] implies integral (sinh,A) = ((number_e - 1) ^2) / (2 * number_e) )
exp_R 1 > 0 by SIN_COS:55;
then A1: 2 * number_e > 0 by IRRAT_1:def 7, XREAL_1:129;
assume A = [.0,1.] ; :: thesis: integral (sinh,A) = ((number_e - 1) ^2) / (2 * number_e)
then A = [.0,jj.] ;
then ( upper_bound A = 1 & lower_bound A = 0 ) by Th37;
then integral (sinh,A) = (((number_e ^2) + 1) / (2 * number_e)) - 1 by Th18, Th19, Th55
.= (((number_e ^2) + 1) / (2 * number_e)) - ((2 * number_e) / (2 * number_e)) by A1, XCMPLX_1:60
.= (((number_e ^2) + 1) - (2 * number_e)) / (2 * number_e) by XCMPLX_1:120
.= (((number_e ^2) - ((2 * number_e) * 1)) + (1 ^2)) / (2 * number_e)
.= ((number_e - 1) ^2) / (2 * number_e) ;
hence integral (sinh,A) = ((number_e - 1) ^2) / (2 * number_e) ; :: thesis: verum