theorem :: SIN_COS7:58

for x being Real st 0 < x holds
log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1)))