let A be non empty closed_interval Subset of REAL; integral ((sinh + cosh),A) = (((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A))) - (sinh . (lower_bound A))
A1:
[#] REAL is open Subset of REAL
;
cosh | A is continuous
by Lm16;
then A2:
cosh is_integrable_on A
by Lm10, INTEGRA5:11;
sinh | A is continuous
by Lm14;
then A3:
sinh is_integrable_on A
by Lm9, INTEGRA5:11;
( cosh | A is bounded & sinh | A is bounded )
by Lm9, Lm10, Lm14, Lm16, INTEGRA5:10;
hence
integral ((sinh + cosh),A) = (((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A))) - (sinh . (lower_bound A))
by A2, A3, A1, Th30, Th31, Th66, SIN_COS2:34, SIN_COS2:35; verum