:: deftheorem Def3 defines Expan_e CLOPBAN4:def 3 :
for n being Nat
for X being Complex_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 ) ) );