theorem Th18: :: NDIFF_1:18

for X being RealNormSpace
for seq being sequence of X st seq is constant holds
( seq is convergent & ( for k being Element of NAT holds lim seq = seq . k ) )