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