:: deftheorem Def4 defines ExpSeq SIN_COS:def 4 :
for z being Complex
for b₂ being Complex_Sequence holds
( b₂ = z ExpSeq iff for n being Nat holds b₂ . n = (z |^ n) / (n !) );