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

proof

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

end;

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