:: deftheorem Def9 defines Conj LOPBAN_4:def 9 :
for X being 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 rExpSeq) . k) * (((Partial_Sums (w rExpSeq)) . n) - ((Partial_Sums (w rExpSeq)) . (n -' k))) ) & ( n < k implies b₅ . k = 0. X ) ) );