for p being Real holds
( cosh is_differentiable_in p & diff (cosh,p) = sinh . p )