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