let A be non empty 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))))
sinh | A is continuous by Lm14;
then A1: cosh `| REAL is_integrable_on A by Lm9, Th31, INTEGRA5:11;
( (cosh `| REAL) | A is bounded & [#] REAL is open Subset of REAL ) by Lm9, Lm14, Th31, INTEGRA5:10;
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