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