:: deftheorem Def3 defines cosh SIN_COS2:def 3 :
for b₁ being Function of REAL,REAL holds
( b₁ = cosh iff for d being Real holds b₁ . d = ((exp_R . d) + (exp_R . (- d))) / 2 );