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;

(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

( 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

then A6:
seq . k is UpperBound of rng (seq ^\ k)
by XXREAL_2:def 1;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;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

(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