let x be real number ; :: thesis: ( x > 0 implies csch" x = sinh" (1 / x) )
assume A1: x > 0 ; :: thesis: csch" x = sinh" (1 / x)
then A2: x ^2 > 0 by SQUARE_1:74;
sinh" (1 / x) = log number_e ,((1 / x) + (sqrt ((1 / (x ^2 )) + (1 ^2 )))) by XCMPLX_1:77
.= log number_e ,((1 / x) + (sqrt ((1 + ((x ^2 ) * 1)) / (x ^2 )))) by A2, XCMPLX_1:114
.= log number_e ,((1 / x) + ((sqrt (1 + (x ^2 ))) / (sqrt (x ^2 )))) by A2, 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 csch" x = sinh" (1 / x) by A1, Def8; :: thesis: verum