let x be Real; :: thesis: ( 0 < x implies log (number_e,x) = tanh" (((x ^2) - 1) / ((x ^2) + 1)) )
assume A1: 0 < x ; :: thesis: log (number_e,x) = tanh" (((x ^2) - 1) / ((x ^2) + 1))
A2: (x ^2) + 1 > 0 by Lm6;
then tanh" (((x ^2) - 1) / ((x ^2) + 1)) = (1 / 2) * (log (number_e,(((((x ^2) - 1) + (((x ^2) + 1) * 1)) / ((x ^2) + 1)) / (1 - (((x ^2) - 1) / ((x ^2) + 1)))))) by XCMPLX_1:113
.= (1 / 2) * (log (number_e,(((2 * (x ^2)) / ((x ^2) + 1)) / (((1 * ((x ^2) + 1)) - ((x ^2) - 1)) / ((x ^2) + 1))))) by A2, XCMPLX_1:127
.= (1 / 2) * (log (number_e,((2 * (x ^2)) / 2))) by A2, XCMPLX_1:55
.= (1 / 2) * (log (number_e,(x to_power 2))) by POWER:46
.= (1 / 2) * (2 * (log (number_e,x))) by A1, Lm1, POWER:55, TAYLOR_1:11
.= log (number_e,x) ;
hence log (number_e,x) = tanh" (((x ^2) - 1) / ((x ^2) + 1)) ; :: thesis: verum