let A be closed-interval Subset of REAL ; :: thesis: ( A = [.0 ,1.] implies integral (sinh + cosh ),A = number_e - 1 )
assume A = [.0 ,1.] ; :: thesis: integral (sinh + cosh ),A = number_e - 1
then A1: ( upper_bound A = 1 & lower_bound A = 0 ) by Th37;
A2: number_e > 0 by IRRAT_1:def 7, SIN_COS:60;
integral (sinh + cosh ),A = (((cosh . 1) - (cosh . 0 )) + (sinh . 1)) - (sinh . 0 ) by A1, Th76
.= ((((number_e ^2 ) + 1) / (2 * number_e )) + (((number_e ^2 ) - 1) / (2 * number_e ))) - 1 by Th17, Th18, Th19, SIN_COS2:16
.= ((((number_e ^2 ) + 1) + ((number_e ^2 ) - 1)) / (2 * number_e )) - 1 by XCMPLX_1:63
.= ((2 * (number_e ^2 )) / (2 * number_e )) - 1
.= ((number_e ^2 ) / number_e ) - 1 by XCMPLX_1:92
.= ((number_e * number_e ) / number_e ) - 1
.= number_e - 1 by A2, XCMPLX_1:90 ;
hence integral (sinh + cosh ),A = number_e - 1 ; :: thesis: verum