let x be real number ; :: 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:65;
then cosh1" (sqrt ((x ^2 ) + 1)) = log number_e ,((sqrt ((x ^2 ) + 1)) + (sqrt (((x ^2 ) + 1) - 1))) by SQUARE_1:def 4
.= log number_e ,((sqrt ((x ^2 ) + 1)) + x) by A1, SQUARE_1:89 ;
hence sinh" x = cosh1" (sqrt ((x ^2 ) + 1)) ; :: thesis: verum