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