theorem Th12: :: LOPBAN_3:12

for X being RealNormSpace
for seq being sequence of X st seq is constant holds
seq is convergent