let A be non empty closed_interval Subset of REAL; :: thesis: integral ((sinh (#) sinh),A) = (((cosh . (upper_bound A)) * (sinh . (upper_bound A))) - ((cosh . (lower_bound A)) * (sinh . (lower_bound A)))) - (integral ((cosh (#) cosh),A))
A1: [#] REAL is open Subset of REAL ;
A2: ( sinh `| REAL is_integrable_on A & (sinh `| REAL) | A is bounded ) by Lm17, Th30;
( cosh `| REAL is_integrable_on A & (cosh `| REAL) | A is bounded ) by Lm15, Th31;
hence integral ((sinh (#) sinh),A) = (((cosh . (upper_bound A)) * (sinh . (upper_bound A))) - ((cosh . (lower_bound A)) * (sinh . (lower_bound A)))) - (integral ((cosh (#) cosh),A)) by A2, A1, Th30, Th31, INTEGRA5:21, SIN_COS2:34, SIN_COS2:35; :: thesis: verum