:: deftheorem defines tanh" SIN_COS7:def 4 :
for x being Real holds tanh" x = (1 / 2) * (log (number_e,((1 + x) / (1 - x))));