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