let x be Real; :: thesis: ( 0 < x implies log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1))) )
assume A1: 0 < x ; :: thesis: log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1)))
then 2 * (tanh" ((x - 1) / (x + 1))) = log (number_e,((((x - 1) + ((x + 1) * 1)) / (x + 1)) / (1 - ((x - 1) / (x + 1))))) by XCMPLX_1:113
.= log (number_e,(((2 * x) / (x + 1)) / (((1 * (x + 1)) - (x - 1)) / (x + 1)))) by A1, XCMPLX_1:127
.= log (number_e,((2 * x) / 2)) by A1, XCMPLX_1:55
.= log (number_e,x) ;
hence log (number_e,x) = 2 * (tanh" ((x - 1) / (x + 1))) ; :: thesis: verum