for k being Nat
for seq being ExtREAL_sequence st seq is convergent holds
( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )