let x be Real; sinh" x = tanh" (x / (sqrt ((x ^2) + 1)))
set t = (sqrt ((x ^2) + 1)) + x;
A1:
(sqrt ((x ^2) + 1)) + x > 0
by Th5;
A2:
(x ^2) + 1 > 0
by Lm6;
A3:
sqrt ((x ^2) + 1) > 0
by Th4;
then tanh" (x / (sqrt ((x ^2) + 1))) =
(1 / 2) * (log (number_e,(((((sqrt ((x ^2) + 1)) * 1) + x) / (sqrt ((x ^2) + 1))) / (1 - (x / (sqrt ((x ^2) + 1)))))))
by XCMPLX_1:113
.=
(1 / 2) * (log (number_e,(((((sqrt ((x ^2) + 1)) * 1) + x) / (sqrt ((x ^2) + 1))) / (((1 * (sqrt ((x ^2) + 1))) - x) / (sqrt ((x ^2) + 1))))))
by A3, XCMPLX_1:127
.=
(1 / 2) * (log (number_e,(((sqrt ((x ^2) + 1)) + x) / ((sqrt ((x ^2) + 1)) - x))))
by A3, XCMPLX_1:55
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / (((sqrt ((x ^2) + 1)) - x) * ((sqrt ((x ^2) + 1)) + x)))))
by A1, XCMPLX_1:91
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / (((sqrt ((x ^2) + 1)) * (sqrt ((x ^2) + 1))) - (x ^2)))))
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / ((sqrt (((x ^2) + 1) ^2)) - (x ^2)))))
by A2, SQUARE_1:29
.=
(1 / 2) * (log (number_e,((((sqrt ((x ^2) + 1)) + x) * ((sqrt ((x ^2) + 1)) + x)) / (((x ^2) + 1) - (x ^2)))))
by A2, SQUARE_1:22
.=
(1 / 2) * (log (number_e,(((sqrt ((x ^2) + 1)) + x) ^2)))
.=
(1 / 2) * (log (number_e,(((sqrt ((x ^2) + 1)) + x) to_power 2)))
by POWER:46
.=
(1 / 2) * (2 * (log (number_e,((sqrt ((x ^2) + 1)) + x))))
by A1, Lm1, POWER:55, TAYLOR_1:11
.=
log (number_e,((sqrt ((x ^2) + 1)) + x))
;
hence
sinh" x = tanh" (x / (sqrt ((x ^2) + 1)))
; verum