let x be real number ; :: thesis: ( 0 <= x implies sinh" x = cosh1" (sqrt ((x ^2 ) + 1)) )
x ^2 >= 0 by XREAL_1:65;
then A1: (x ^2 ) + 1 >= 0 + 1 by XREAL_1:9;
assume A2: 0 <= x ; :: thesis: sinh" x = cosh1" (sqrt ((x ^2 ) + 1))
cosh1" (sqrt ((x ^2 ) + 1)) = log number_e ,((sqrt ((x ^2 ) + 1)) + (sqrt (((x ^2 ) + 1) - 1))) by A1, SQUARE_1:def 4
.= log number_e ,((sqrt ((x ^2 ) + 1)) + x) by A2, SQUARE_1:89 ;
hence sinh" x = cosh1" (sqrt ((x ^2 ) + 1)) ; :: thesis: verum