:: deftheorem Def5 defines Conj CLOPBAN4:def 5 :
for X being Complex_Banach_Algebra
for z, w being Element of X
for n being Nat
for b₅ being sequence of X 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. X ) ) );