for seq being Real_Sequence st seq is constant holds
for n being Nat holds lim seq = seq . n by Th25;