theorem :: SIN_COS7:59

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