let seq be ExtREAL_sequence; :: thesis: 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 )
let k be Element of NAT ; :: thesis: ( seq is non-increasing & -infty < seq . k & seq . k < +infty implies ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k ) )
assume that
A1: seq is non-increasing and
A2: -infty < seq . k and
A3: seq . k < +infty ; :: thesis: ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k )
set seq0 = seq ^\ k;

now :: thesis: for y being ExtReal st y in rng (seq ^\ k) holds
y <= seq . k

let y be ExtReal; :: thesis: ( y in rng (seq ^\ k) implies y <= seq . k )
assume y in rng (seq ^\ k) ; :: thesis: y <= seq . k
then consider n being object such that
A4: n in dom (seq ^\ k) and
A5: y = (seq ^\ k) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A4;
k <= n + k by NAT_1:11;
then seq . (n + k) <= seq . k by A1, Th7;
hence y <= seq . k by A5, NAT_1:def 3; :: thesis: verum

end;

then A6: seq . k is UpperBound of rng (seq ^\ k) by XXREAL_2:def 1;
(seq ^\ k) . 0 = seq . (0 + k) by NAT_1:def 3;
then A7: seq . k in rng (seq ^\ k) by FUNCT_2:4;
seq . k in REAL by A2, A3, XXREAL_0:14;
then rng (seq ^\ k) is bounded_above by A6, XXREAL_2:def 10;
hence ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k ) by A6, A7, XXREAL_2:55; :: thesis: verum