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 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:62, TAYLOR_1:11
.= (1 / 2) * (log number_e ,(((1 + x) * (1 - y)) / ((1 - x) * (1 + y)))) by XCMPLX_1:85
.= (1 / 2) * (log number_e ,((((1 - y) + x) - (x * y)) / (((1 + y) - x) - (x * y)))) ;
A4: 1 - (x * y) <> 0 by A1, Th28;
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:114
.= (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:128
.= (1 / 2) * (log number_e ,((((1 - y) + x) - (x * y)) / (((1 + y) - x) - (x * y)))) by A4, XCMPLX_1:55 ;
hence (tanh" x) - (tanh" y) = tanh" ((x - y) / (1 - (x * y))) by A3; :: thesis: verum