:: deftheorem Def2 defines rExpSeq LOPBAN_4:def 2 :
for X being Banach_Algebra
for z being Element of X
for b₃ being sequence of X holds
( b₃ = z rExpSeq iff for n being Nat holds b₃ . n = (1 / (n !)) * (z #N n) );