for X being RealNormSpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
seq1 is convergent