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 that
A1: seq is non-decreasing and
A2: -infty < seq . k and
A3: seq . k < +infty ; :: thesis: ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k )
set seq0 = seq ^\ k;
now :: thesis: for y being ExtReal st y in rng (seq ^\ k) holds
seq . k <= y
let y be ExtReal; :: thesis: ( y in rng (seq ^\ k) implies seq . k <= y )
assume y in rng (seq ^\ k) ; :: thesis: seq . k <= y
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 . k <= seq . (n + k) by A1, Th7;
hence seq . k <= y by A5, NAT_1:def 3; :: thesis: verum
end;
then A6: seq . k is LowerBound of rng (seq ^\ k) by XXREAL_2:def 2;
(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_below by A6, XXREAL_2:def 9;
hence ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) by A6, A7, XXREAL_2:56; :: thesis: verum