for seq1, seq2 being Real_Sequence
for k being positive Real st ( for n being Nat holds
( seq1 . n = (seq2 . n) to_power k & seq2 . n >= 0 ) ) holds
( seq1 is convergent iff seq2 is convergent )