for X being RealNormSpace
for seq being sequence of X st seq is convergent holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )