let A be non empty closed_interval Subset of REAL; :: thesis: for r being Real holds integral ((r (#) sinh),A) = (r * (cosh . (upper_bound A))) - (r * (cosh . (lower_bound A)))
let r be Real; :: thesis: integral ((r (#) sinh),A) = (r * (cosh . (upper_bound A))) - (r * (cosh . (lower_bound A)))
A1: [#] REAL is open Subset of REAL ;
( sinh | A is continuous & sinh | A is bounded ) by Lm9, Lm14, INTEGRA5:10;
hence integral ((r (#) sinh),A) = (r * (cosh . (upper_bound A))) - (r * (cosh . (lower_bound A))) by A1, Lm9, Th31, Th68, INTEGRA5:11, SIN_COS2:35; :: thesis: verum