:: deftheorem Def3 defines sinh_C SIN_COS3:def 3 :
for b₁ being Function of COMPLEX,COMPLEX holds
( b₁ = sinh_C iff for z being Complex holds b₁ . z = ((exp z) - (exp (- z))) / 2 );