:: deftheorem Def1 defines ExpSeq CLOPBAN4:def 1 :
for X being Complex_Banach_Algebra
for z being Element of X
for b₃ being sequence of X holds
( b₃ = z ExpSeq iff for n being Nat holds b₃ . n = (1r / (n !)) * (z #N n) );