theorem Th17: :: SIN_COS2:17

for p being Real holds tanh . p = (sinh . p) / (cosh . p)