:: deftheorem Def9 defines GeoSeq LOPBAN_3:def 9 :
for X being Banach_Algebra
for z being Element of X
for b₃ being sequence of X holds
( b₃ = z GeoSeq iff ( b₃ . 0 = 1. X & ( for n being Nat holds b₃ . (n + 1) = (b₃ . n) * z ) ) );