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