for seq, seq2 being Real_Sequence
for k being positive Real st seq is convergent & ( for n being Nat holds seq2 . n = |.((lim seq) - (seq . n)).| to_power k ) holds
( seq2 is convergent & lim seq2 = 0 )