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