:: deftheorem Def11 defines Alfa SIN_COS:def 11 :
for n being Nat
for z, w being Complex
for b₄ being Complex_Sequence holds
( b₄ = Alfa (n,z,w) iff for k being Nat holds
( ( k <= n implies b₄ . k = ((z ExpSeq) . k) * ((Partial_Sums (w ExpSeq)) . (n -' k)) ) & ( n < k implies b₄ . k = 0 ) ) );