:: deftheorem Def8 defines Alfa LOPBAN_4:def 8 :
for n being Nat
for X being Banach_Algebra
for z, w being Element of X
for b₅ being sequence of X holds
( b₅ = Alfa (n,z,w) iff for k being Nat holds
( ( k <= n implies b₅ . k = ((z rExpSeq) . k) * ((Partial_Sums (w rExpSeq)) . (n -' k)) ) & ( n < k implies b₅ . k = 0. X ) ) );