:: deftheorem Def7 defines Expan_e LOPBAN_4:def 7 :
for n being Nat
for X being Banach_Algebra
for z, w being Element of X
for b₅ being sequence of X holds
( b₅ = Expan_e (n,z,w) iff for k being Nat holds
( ( k <= n implies b₅ . k = (((Coef_e n) . k) * (z #N k)) * (w #N (n -' k)) ) & ( n < k implies b₅ . k = 0. X ) ) );