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