:: deftheorem Def1 defines sin_C SIN_COS3:def 1 :
for b₁ being Function of COMPLEX,COMPLEX holds
( b₁ = sin_C iff for z being Complex holds b₁ . z = ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>) );