let x be real number ; :: thesis: ( x >= 1 implies cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2))) )
assume x >= 1 ; :: thesis: cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2)))
then A1: ( sqrt ((x + 1) / 2) >= 1 & (x + 1) / 2 >= 0 & (x - 1) / 2 >= 0 & (sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0 & ((x ^2 ) - 1) / 4 >= 0 ) by Th7, Th8, Th9, Th10;
then 2 * (sinh" (sqrt ((x - 1) / 2))) = 2 * (log number_e ,((sqrt ((x - 1) / 2)) + (sqrt (((x - 1) / 2) + 1)))) by SQUARE_1:def 4
.= log number_e ,(((sqrt ((x - 1) / 2)) + (sqrt ((x + 1) / 2))) to_power 2) by A1, Lm2, POWER:63
.= log number_e ,(((sqrt ((x - 1) / 2)) + (sqrt ((x + 1) / 2))) ^2 ) by POWER:53
.= log number_e ,((((sqrt ((x - 1) / 2)) ^2 ) + ((2 * (sqrt ((x - 1) / 2))) * (sqrt ((x + 1) / 2)))) + ((sqrt ((x + 1) / 2)) ^2 ))
.= log number_e ,((((x - 1) / 2) + ((2 * (sqrt ((x - 1) / 2))) * (sqrt ((x + 1) / 2)))) + ((sqrt ((x + 1) / 2)) ^2 )) by A1, SQUARE_1:def 4
.= log number_e ,((((x - 1) / 2) + ((2 * (sqrt ((x - 1) / 2))) * (sqrt ((x + 1) / 2)))) + ((x + 1) / 2)) by A1, SQUARE_1:def 4
.= log number_e ,(x + (2 * ((sqrt ((x - 1) / 2)) * (sqrt ((x + 1) / 2)))))
.= log number_e ,(x + (2 * (sqrt (((x - 1) / 2) * ((x + 1) / 2))))) by A1, SQUARE_1:97
.= log number_e ,(x + ((sqrt (2 ^2 )) * (sqrt (((x ^2 ) - 1) / 4)))) by SQUARE_1:89
.= log number_e ,(x + (sqrt (4 * (((x ^2 ) - 1) / 4)))) by A1, SQUARE_1:97
.= log number_e ,(x + (sqrt ((x ^2 ) - 1))) ;
hence cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2))) ; :: thesis: verum