theorem :: CFCONT_1:28

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