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: ( cosh `| REAL is_integrable_on A & (cosh `| REAL ) | A is bounded ) by Lm11, Th31;
A2: ( sinh `| REAL is_integrable_on A & (sinh `| REAL ) | A is bounded ) by Lm13, Th30;
[#] REAL is open Subset of REAL ;
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 A1, A2, Th30, Th31, INTEGRA5:21, SIN_COS2:34, SIN_COS2:35; :: thesis: verum