theorem Th31: :: SIN_COS2:31

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