:: deftheorem Def1 defines GeoSeq COMSEQ_3:def 1 :
for z being Complex
for b₂ being Complex_Sequence holds
( b₂ = z GeoSeq iff ( b₂ . 0 = 1r & ( for n being Nat holds b₂ . (n + 1) = (b₂ . n) * z ) ) );