for seq being Complex_Sequence st seq is convergent & lim seq <> 0 holds
ex k being Nat st seq ^\ k is non-zero