theorem Th26: :: RINFSUP2:26

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