let x be Real; :: thesis: ( 0 <= x implies sinh" x = cosh1" (sqrt ((x ^2) + 1)) )
assume A1: 0 <= x ; :: thesis: sinh" x = cosh1" (sqrt ((x ^2) + 1))
x ^2 >= 0 by XREAL_1:63;
then cosh1" (sqrt ((x ^2) + 1)) = log (number_e,((sqrt ((x ^2) + 1)) + (sqrt (((x ^2) + 1) - 1)))) by SQUARE_1:def 2
.= log (number_e,((sqrt ((x ^2) + 1)) + x)) by A1, SQUARE_1:22 ;
hence sinh" x = cosh1" (sqrt ((x ^2) + 1)) ; :: thesis: verum