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