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