for X being RealNormSpace
for seq, seq1 being sequence of X
for k being Nat st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th7, Th8;