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