let A be closed-interval Subset of REAL ; :: thesis: for r being Real holds integral (r (#) cosh ),A = (r * (sinh . (upper_bound A))) - (r * (sinh . (lower_bound A)))
let r be Real; :: thesis: integral (r (#) cosh ),A = (r * (sinh . (upper_bound A))) - (r * (sinh . (lower_bound A)))
A1: [#] REAL is open Subset of REAL ;
( cosh | A is continuous & cosh | A is bounded ) by Lm10, Lm16, INTEGRA5:10;
hence integral (r (#) cosh ),A = (r * (sinh . (upper_bound A))) - (r * (sinh . (lower_bound A))) by A1, Lm10, Th30, Th68, INTEGRA5:11, SIN_COS2:34; :: thesis: verum