for g being Complex
for seq being Complex_Sequence st ( ( seq is constant & g in rng seq ) or ( seq is constant & ex n being Nat st seq . n = g ) ) holds
lim seq = g