for seq being Complex_Sequence st seq is constant holds
for n being Nat holds lim seq = seq . n by Th27;