let x be real number ; :: thesis: ( x > 0 & x <= 1 implies sech2" x = cosh2" (1 / x) )
assume A1: ( x > 0 & x <= 1 ) ; :: thesis: sech2" x = cosh2" (1 / x)
then A2: x ^2 > 0 by SQUARE_1:74;
A3: ( 1 / x >= 1 & 1 - (x ^2 ) >= 0 ) by A1, Lm1, Th22, XREAL_1:87;
cosh2" (1 / x) = - (log number_e ,((1 / x) + (sqrt ((1 / (x ^2 )) - (1 ^2 ))))) by XCMPLX_1:77
.= - (log number_e ,((1 / x) + (sqrt ((1 - (1 * (x ^2 ))) / (x ^2 ))))) by A2, XCMPLX_1:127
.= - (log number_e ,((1 / x) + ((sqrt (1 - (x ^2 ))) / (sqrt (x ^2 ))))) by A2, A3, SQUARE_1:99
.= - (log number_e ,((1 / x) + ((sqrt (1 - (x ^2 ))) / x))) by A1, SQUARE_1:89
.= - (log number_e ,((1 + (sqrt (1 - (x ^2 )))) / x)) ;
hence sech2" x = cosh2" (1 / x) ; :: thesis: verum