for x being Real st x ^2 < 1 holds
tanh" x = sinh" (x / (sqrt (1 - (x ^2))))