:: deftheorem Def9 defines Expan SIN_COS:def 9 :
for n being Nat
for z, w being Complex
for b₄ being Complex_Sequence holds
( b₄ = Expan (n,z,w) iff for k being Nat holds
( ( k <= n implies b₄ . k = (((Coef n) . k) * (z |^ k)) * (w |^ (n -' k)) ) & ( n < k implies b₄ . k = 0 ) ) );