for X being RealUnitarySpace
for seq being sequence of X
for k being Nat st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq ) by Th10;