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