theorem Th34: :: SIN_COS2:34

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