:: deftheorem Def4 defines cosh_C SIN_COS3:def 4 :
for b₁ being Function of COMPLEX,COMPLEX holds
( b₁ = cosh_C iff for z being Complex holds b₁ . z = ((exp z) + (exp (- z))) / 2 );