let x be real number ; :: thesis: ( 0 < x & x < 1 implies tanh" x = cosh1" (1 / (sqrt (1 - (x ^2 )))) )
assume A1: ( 0 < x & x < 1 ) ; :: thesis: tanh" x = cosh1" (1 / (sqrt (1 - (x ^2 ))))
then (1 + x) / (1 - x) > 0 by Th15;
then A2: sqrt ((1 + x) / (1 - x)) = ((1 + x) / (1 - x)) to_power (1 / 2) by ASYMPT_1:89;
A3: ( 1 - x > 0 & 1 + x > 0 & x ^2 < 1 & 1 - (x ^2 ) > 0 & 1 / (sqrt (1 - (x ^2 ))) > 1 & (1 + x) / (1 - x) > 0 ) by A1, Lm7, Th15, Th16, Th17, XREAL_1:52;
then A4: sqrt (1 + x) > 0 by SQUARE_1:93;
A5: x ^2 >= 0 by XREAL_1:65;
cosh1" (1 / (sqrt (1 - (x ^2 )))) = log number_e ,((1 / (sqrt (1 - (x ^2 )))) + (sqrt ((1 / ((sqrt (1 - (x ^2 ))) ^2 )) - (1 ^2 )))) by XCMPLX_1:77
.= log number_e ,((1 / (sqrt (1 - (x ^2 )))) + (sqrt ((1 / (1 - (x ^2 ))) - 1))) by A3, SQUARE_1:def 4
.= log number_e ,((1 / (sqrt (1 - (x ^2 )))) + (sqrt ((1 - (1 * (1 - (x ^2 )))) / (1 - (x ^2 ))))) by A3, XCMPLX_1:127
.= log number_e ,((1 / (sqrt (1 - (x ^2 )))) + ((sqrt (x ^2 )) / (sqrt (1 - (x ^2 ))))) by A3, A5, SQUARE_1:99
.= log number_e ,((1 / (sqrt (1 - (x ^2 )))) + (x / (sqrt (1 - (x ^2 ))))) by A1, SQUARE_1:89
.= log number_e ,((1 + x) / (sqrt ((1 - x) * (1 + x))))
.= log number_e ,((1 + x) / ((sqrt (1 - x)) * (sqrt (1 + x)))) by A3, SQUARE_1:97
.= log number_e ,((sqrt ((1 + x) ^2 )) / ((sqrt (1 - x)) * (sqrt (1 + x)))) by A3, SQUARE_1:89
.= log number_e ,(((sqrt (1 + x)) * (sqrt (1 + x))) / ((sqrt (1 - x)) * (sqrt (1 + x)))) by A3, SQUARE_1:97
.= log number_e ,((sqrt (1 + x)) / (sqrt (1 - x))) by A4, XCMPLX_1:92
.= log number_e ,(sqrt ((1 + x) / (1 - x))) by A3, SQUARE_1:99
.= (1 / 2) * (log number_e ,((1 + x) / (1 - x))) by A2, A3, Lm2, POWER:63 ;
hence tanh" x = cosh1" (1 / (sqrt (1 - (x ^2 )))) ; :: thesis: verum