for seq being ExtREAL_sequence
for k being Element of NAT st seq is non-increasing & -infty < seq . k & seq . k < +infty holds
( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k )