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