:: deftheorem defines cosh1" SIN_COS7:def 2 :
for x being Real holds cosh1" x = log (number_e,(x + (sqrt ((x ^2) - 1))));