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;

(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

( 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

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

(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