let x, y be real number ; :: 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 Lm5;
A3: (x * y) + 1 <> 0 by A1, Th27;
A4: (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, Lm2, POWER:61
.= (1 / 2) * (log number_e ,(((1 + x) * (1 + y)) / ((1 - x) * (1 - y)))) by XCMPLX_1:77
.= (1 / 2) * (log number_e ,((((1 + x) + y) + (x * y)) / (((1 + (x * y)) - x) - y))) ;
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 A3, XCMPLX_1:114
.= (1 / 2) * (log number_e ,(((((x + y) + 1) + (x * y)) / (1 + (x * y))) / (((1 * (1 + (x * y))) - (x + y)) / (1 + (x * y))))) by A3, XCMPLX_1:128
.= (1 / 2) * (log number_e ,((((1 + x) + y) + (x * y)) / (((1 + (x * y)) - x) - y))) by A3, XCMPLX_1:55 ;
hence (tanh" x) + (tanh" y) = tanh" ((x + y) / (1 + (x * y))) by A4; :: thesis: verum