:: deftheorem Def5 defines tanh SIN_COS2:def 5 :
for b₁ being Function of REAL,REAL holds
( b₁ = tanh iff for d being Real holds b₁ . d = ((exp_R . d) - (exp_R . (- d))) / ((exp_R . d) + (exp_R . (- d))) );