let A be closed-interval Subset of REAL ; :: thesis: integral (sinh (#) cosh ),A = (1 / 2) * (((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A))))
X: A c= dom sinh by D5;
sinh | A is continuous by Lm10;
then A1: ( cosh `| REAL is_integrable_on A & (cosh `| REAL ) | A is bounded ) by Th31, X, INTEGRA5:10, INTEGRA5:11;
[#] REAL is open Subset of REAL ;
then integral (sinh (#) cosh ),A = (((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A)))) - (integral (sinh (#) cosh ),A) by A1, Th31, INTEGRA5:21, SIN_COS2:35;
hence integral (sinh (#) cosh ),A = (1 / 2) * (((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A)))) ; :: thesis: verum