theorem Th16: :: RINFSUP2:16

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