:: deftheorem Def24 defines P_dt SIN_COS:def 24 :
for z being Complex
for b₂ being Complex_Sequence holds
( b₂ = z P_dt iff for n being Nat holds b₂ . n = (z |^ (n + 1)) / ((n + 2) !) );