let A be non empty closed_interval Subset of REAL; :: thesis: integral (cosh,A) = (sinh . (upper_bound A)) - (sinh . (lower_bound A))
A1: for x being Element of REAL st x in dom (sinh `| REAL) holds
(sinh `| REAL) . x = cosh . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (sinh `| REAL) implies (sinh `| REAL) . x = cosh . x )
assume x in dom (sinh `| REAL) ; :: thesis: (sinh `| REAL) . x = cosh . x
(sinh `| REAL) . x = diff (sinh,x) by FDIFF_1:def 7, SIN_COS2:34;
hence (sinh `| REAL) . x = cosh . x by SIN_COS2:34; :: thesis: verum

end;

A2: ( cosh is_integrable_on A & cosh | A is bounded ) by Lm17;
dom (sinh `| REAL) = dom cosh by FDIFF_1:def 7, SIN_COS2:30, SIN_COS2:34;
then sinh `| REAL = cosh by A1, PARTFUN1:5;
hence integral (cosh,A) = (sinh . (upper_bound A)) - (sinh . (lower_bound A)) by A2, INTEGRA5:13, SIN_COS2:34; :: thesis: verum