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