let A be 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