:: deftheorem Def14 defines exp SIN_COS:def 14 :
for b₁ being Function of COMPLEX,COMPLEX holds
( b₁ = exp iff for z being Complex holds b₁ . z = Sum (z ExpSeq) );