for seq being Complex_Sequence
for z being Complex st 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Nat holds seq . (n + 1) = (seq . n) * z ) holds
( seq is convergent & lim seq = 0c )