theorem Th25: :: RINFSUP2:25

for k being Nat
for seq being ExtREAL_sequence st seq is non-increasing holds
( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) )