let x be real number ; :: thesis: ( x >= 1 implies cosh1" x = sinh" (sqrt ((x ^2 ) - 1)) )
assume A1: x >= 1 ; :: thesis: cosh1" x = sinh" (sqrt ((x ^2 ) - 1))
then (x ^2 ) - 1 >= 0 by Lm4;
then sinh" (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 cosh1" x = sinh" (sqrt ((x ^2 ) - 1)) ; :: thesis: verum