for k being Nat
for seq being Real_Sequence st seq ^\ k is convergent holds
seq is convergent