let x be real number ; :: thesis: ( x ^2 < 1 implies tanh" x = sinh" (x / (sqrt (1 - (x ^2 )))) )
assume x ^2 < 1 ; :: thesis: tanh" x = sinh" (x / (sqrt (1 - (x ^2 ))))
then A1: ( 1 - (x ^2 ) > 0 & x + 1 > 0 & 1 - x > 0 & (x + 1) / (1 - x) > 0 ) by Lm5, Th11, XREAL_1:52;
then A2: sqrt (x + 1) > 0 by SQUARE_1:93;
A3: sqrt ((x + 1) / (1 - x)) = ((x + 1) / (1 - x)) to_power (1 / 2) by A1, ASYMPT_1:89;
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:77
.= log number_e ,((x / (sqrt (1 - (x ^2 )))) + (sqrt (((x ^2 ) / (1 - (x ^2 ))) + 1))) by A1, SQUARE_1:def 4
.= log number_e ,((x / (sqrt (1 - (x ^2 )))) + (sqrt (((x ^2 ) + ((1 - (x ^2 )) * 1)) / (1 - (x ^2 ))))) by A1, XCMPLX_1:114
.= log number_e ,((x / (sqrt (1 - (x ^2 )))) + ((sqrt 1) / (sqrt (1 - (x ^2 ))))) by A1, SQUARE_1:99
.= log number_e ,((x + 1) / (sqrt ((1 - x) * (1 + x)))) by SQUARE_1:83
.= log number_e ,((sqrt ((x + 1) ^2 )) / (sqrt ((1 - x) * (1 + x)))) by A1, SQUARE_1:89
.= log number_e ,(((sqrt (x + 1)) * (sqrt (x + 1))) / (sqrt ((1 - x) * (1 + x)))) by A1, SQUARE_1:97
.= log number_e ,(((sqrt (x + 1)) * (sqrt (x + 1))) / ((sqrt (1 - x)) * (sqrt (1 + x)))) by A1, SQUARE_1:97
.= log number_e ,((sqrt (x + 1)) / (sqrt (1 - x))) by A2, XCMPLX_1:92
.= log number_e ,(sqrt ((x + 1) / (1 - x))) by A1, SQUARE_1:99
.= (1 / 2) * (log number_e ,((1 + x) / (1 - x))) by A1, A3, Lm2, POWER:63 ;
hence tanh" x = sinh" (x / (sqrt (1 - (x ^2 )))) ; :: thesis: verum