let A be closed-interval Subset of REAL ; :: thesis: integral (sinh + cosh ),A = (((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A))) - (sinh . (lower_bound A))
X: A c= dom cosh by D6;
cosh | A is continuous by Lm12;
then A1: ( cosh is_integrable_on A & cosh | A is bounded ) by X, INTEGRA5:10, INTEGRA5:11;
Y: A c= dom sinh by D5;
sinh | A is continuous by Lm10;
then A2: ( sinh is_integrable_on A & sinh | A is bounded ) by Y, INTEGRA5:10, INTEGRA5:11;
[#] REAL is open Subset of REAL ;
hence integral (sinh + cosh ),A = (((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A))) - (sinh . (lower_bound A)) by A1, A2, Th30, Th31, Th66, SIN_COS2:34, SIN_COS2:35; :: thesis: verum