theorem Th20: :: RINFSUP2:20

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