let A be non empty closed_interval Subset of REAL; ( 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.]
; 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
; verum