theorem :: SIN_COS8:5

for x being Real holds
( cosh x = 1 / (sqrt (1 - ((tanh x) ^2))) & sinh x = (tanh x) / (sqrt (1 - ((tanh x) ^2))) )