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