let x be Real; :: thesis: ( x ^2 < 1 implies tanh" x = sinh" (x / (sqrt (1 - (x ^2)))) )
assume A1: x ^2 < 1 ; :: thesis: tanh" x = sinh" (x / (sqrt (1 - (x ^2))))
then A2: x + 1 > 0 by Th11;
A3: sqrt (x + 1) > 0 by A1, Th11, SQUARE_1:25;
A4: (x + 1) / (1 - x) > 0 by A1, Lm4;
A5: 1 - (x ^2) > 0 by A1, XREAL_1:50;
A6: 1 - x > 0 by A1, Th11;
then A7: sqrt ((x + 1) / (1 - x)) = ((x + 1) / (1 - x)) to_power (1 / 2) by A2, ASYMPT_1:83;
sinh" (x / (sqrt (1 - (x ^2)))) = log (number_e,((x / (sqrt (1 - (x ^2)))) + (sqrt (((x ^2) / ((sqrt (1 - (x ^2))) ^2)) + 1)))) by XCMPLX_1:76
.= log (number_e,((x / (sqrt (1 - (x ^2)))) + (sqrt (((x ^2) / (1 - (x ^2))) + 1)))) by A5, SQUARE_1:def 2
.= log (number_e,((x / (sqrt (1 - (x ^2)))) + (sqrt (((x ^2) + ((1 - (x ^2)) * 1)) / (1 - (x ^2)))))) by A5, XCMPLX_1:113
.= log (number_e,((x / (sqrt (1 - (x ^2)))) + ((sqrt 1) / (sqrt (1 - (x ^2)))))) by A5, SQUARE_1:30
.= log (number_e,((x + 1) / (sqrt ((1 - x) * (1 + x)))))
.= log (number_e,((sqrt ((x + 1) ^2)) / (sqrt ((1 - x) * (1 + x))))) by A2, SQUARE_1:22
.= log (number_e,(((sqrt (x + 1)) * (sqrt (x + 1))) / (sqrt ((1 - x) * (1 + x))))) by A2, SQUARE_1:29
.= log (number_e,(((sqrt (x + 1)) * (sqrt (x + 1))) / ((sqrt (1 - x)) * (sqrt (1 + x))))) by A2, A6, SQUARE_1:29
.= log (number_e,((sqrt (x + 1)) / (sqrt (1 - x)))) by A3, XCMPLX_1:91
.= log (number_e,(sqrt ((x + 1) / (1 - x)))) by A2, A6, SQUARE_1:30
.= (1 / 2) * (log (number_e,((1 + x) / (1 - x)))) by A4, A7, Lm1, POWER:55, TAYLOR_1:11 ;
hence tanh" x = sinh" (x / (sqrt (1 - (x ^2)))) ; :: thesis: verum