let p be real number ; :: thesis: ( sinh is_differentiable_on REAL & diff sinh ,p = cosh . p )
( [#] REAL is open Subset of REAL & REAL c= dom sinh & ( for p being Real st p in REAL holds
sinh is_differentiable_in p ) ) by Th31, FUNCT_2:def 1;
hence ( sinh is_differentiable_on REAL & diff sinh ,p = cosh . p ) by Th31, FDIFF_1:16; :: thesis: verum