let seq be ExtREAL_sequence; :: thesis: for k being Element of NAT st seq is non-decreasing & -infty < seq . k & seq . k < +infty holds
( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k )
let k be Element of NAT ; :: thesis: ( seq is non-decreasing & -infty < seq . k & seq . k < +infty implies ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) )
assume A1: ( seq is non-decreasing & -infty < seq . k & seq . k < +infty ) ; :: thesis: ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k )
set seq0 = seq ^\ k;

now

let y be ext-real number ; :: thesis: ( y in rng (seq ^\ k) implies seq . k <= y )
assume y in rng (seq ^\ k) ; :: thesis: seq . k <= y
then consider n being set such that
A2: ( n in dom (seq ^\ k) & y = (seq ^\ k) . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A2;
k <= n + k by NAT_1:11;
then seq . k <= seq . (n + k) by A1, Th7;
hence seq . k <= y by A2, NAT_1:def 3; :: thesis: verum

end;

then A3: seq . k is LowerBound of rng (seq ^\ k) by XXREAL_2:def 2;
seq . k in REAL by A1, XXREAL_0:14;
then A4: rng (seq ^\ k) is bounded_below by A3, SUPINF_1:def 12;
(seq ^\ k) . 0 = seq . (0 + k) by NAT_1:def 3;
then seq . k in rng (seq ^\ k) by FUNCT_2:6;
hence ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) by A3, A4, Def3, XXREAL_2:56; :: thesis: verum