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

end;

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