let x be Real; :: 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 Lm3;
then sinh" (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 cosh1" x = sinh" (sqrt ((x ^2) - 1)) ; :: thesis: verum