theorem :: SIN_COS7:35

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