let x be Real; :: thesis: ( x > 0 & x <= 1 implies sech1" x = cosh1" (1 / x) )
assume that
A1: x > 0 and
A2: x <= 1 ; :: thesis: sech1" x = cosh1" (1 / x)
A3: 1 - (x ^2) >= 0 by A1, A2, Th22;
A4: x ^2 > 0 by A1;
cosh1" (1 / x) = log (number_e,((1 / x) + (sqrt ((1 / (x ^2)) - (1 ^2))))) by XCMPLX_1:76
.= log (number_e,((1 / x) + (sqrt ((1 - (1 * (x ^2))) / (x ^2))))) by A4, XCMPLX_1:126
.= log (number_e,((1 / x) + ((sqrt (1 - (x ^2))) / (sqrt (x ^2))))) by A1, A3, SQUARE_1:30
.= log (number_e,((1 / x) + ((sqrt (1 - (x ^2))) / x))) by A1, SQUARE_1:22
.= log (number_e,((1 + (sqrt (1 - (x ^2)))) / x)) ;
hence sech1" x = cosh1" (1 / x) ; :: thesis: verum