theorem Th35: :: SIN_COS2:35

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