let x be Real; ( x ^2 < 1 implies tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2)))) )
assume A1:
x ^2 < 1
; tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2))))
then A2:
(1 - (x ^2)) ^2 > 0
by Th12;
A3:
x + 1 > 0
by A1, Th11;
(1 / 2) * (sinh" ((2 * x) / (1 - (x ^2)))) =
(1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (sqrt ((((2 * x) ^2) / ((1 - (x ^2)) ^2)) + 1)))))
by XCMPLX_1:76
.=
(1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (sqrt (((4 * (x ^2)) + (((1 - (x ^2)) ^2) * 1)) / ((1 - (x ^2)) ^2))))))
by A2, XCMPLX_1:113
.=
(1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (sqrt ((((x ^2) + 1) ^2) / ((1 - (x ^2)) ^2))))))
.=
(1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (sqrt ((((x ^2) + 1) / (1 - (x ^2))) ^2)))))
by XCMPLX_1:76
.=
(1 / 2) * (log (number_e,(((2 * x) / (1 - (x ^2))) + (((x ^2) + 1) / (1 - (x ^2))))))
by A1, Th13, SQUARE_1:22
.=
(1 / 2) * (log (number_e,(((2 * x) + ((x ^2) + 1)) / (1 - (x ^2)))))
.=
(1 / 2) * (log (number_e,(((x + 1) * (x + 1)) / ((1 - x) * (1 + x)))))
.=
(1 / 2) * (log (number_e,((x + 1) / (1 - x))))
by A3, XCMPLX_1:91
;
hence
tanh" x = (1 / 2) * (sinh" ((2 * x) / (1 - (x ^2))))
; verum