let A be non empty closed_interval Subset of REAL; :: thesis: ( A = [.0,1.] implies integral ((sinh + cosh),A) = number_e - 1 )
A1: number_e > 0 by IRRAT_1:def 7, SIN_COS:55;
assume A = [.0,1.] ; :: thesis: integral ((sinh + cosh),A) = number_e - 1
then ( upper_bound A = 1 & lower_bound A = 0 ) by Th37;
then integral ((sinh + cosh),A) = (((cosh . 1) - (cosh . 0)) + (sinh . 1)) - (sinh . 0) by 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:62
.= ((2 * (number_e ^2)) / (2 * number_e)) - 1
.= ((number_e ^2) / number_e) - 1 by XCMPLX_1:91
.= ((number_e * number_e) / number_e) - 1
.= number_e - 1 by A1, XCMPLX_1:89 ;
hence integral ((sinh + cosh),A) = number_e - 1 ; :: thesis: verum