theorem Th17: :: RINFSUP2:17

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