let x, y be Real; ( 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 )
; (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:54, TAYLOR_1:11
.=
(1 / 2) * (log (number_e,(((1 + x) * (1 - y)) / ((1 - x) * (1 + y)))))
by XCMPLX_1:84
.=
(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: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 - 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; verum