let A be closed-interval Subset of REAL ; :: thesis: integral cosh ,A = (sinh . (upper_bound A)) - (sinh . (lower_bound A))
A1: ( cosh is_integrable_on A & cosh | A is bounded ) by Lm13;
dom (sinh `| REAL ) = REAL by FDIFF_1:def 8, SIN_COS2:34;
then A2: dom (sinh `| REAL ) = dom cosh by SIN_COS2:30;
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 8, SIN_COS2:34;
hence (sinh `| REAL ) . x = cosh . x by SIN_COS2:34; :: thesis: verum

end;

then sinh `| REAL = cosh by A2, PARTFUN1:34;
hence integral cosh ,A = (sinh . (upper_bound A)) - (sinh . (lower_bound A)) by A1, INTEGRA5:13, SIN_COS2:34; :: thesis: verum