theorem Th32: :: SIN_COS2:32

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