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