let seq be sequence of REAL; :: thesis: for Eseq being sequence of ExtREAL st seq = Eseq & seq is bounded_below holds
lower_bound seq = inf (rng Eseq)
let Eseq be sequence of ExtREAL; :: thesis: ( seq = Eseq & seq is bounded_below implies lower_bound seq = inf (rng Eseq) )
assume that
A1: seq = Eseq and
A2: seq is bounded_below ; :: thesis: lower_bound seq = inf (rng Eseq)
reconsider s = lower_bound seq as R_eal by XXREAL_0:def 1;
A3: dom Eseq = NAT by FUNCT_2:def 1;
A4: rng Eseq <> {+infty}

proof

assume rng Eseq = {+infty} ; :: thesis: contradiction
then reconsider k1 = +infty as Element of rng Eseq by TARSKI:def 1;
consider n1 being object such that
A5: n1 in NAT and
Eseq . n1 = k1 by A3, FUNCT_1:def 3;
reconsider n1 = n1 as Element of NAT by A5;
seq . n1 = k1 by A1;
hence contradiction ; :: thesis: verum

end;

for x being ExtReal st x in rng Eseq holds
s <= x

proof

let x be ExtReal; :: thesis: ( x in rng Eseq implies s <= x )
assume x in rng Eseq ; :: thesis: s <= x
then ex n1 being object st
( n1 in NAT & Eseq . n1 = x ) by A3, FUNCT_1:def 3;
hence s <= x by A1, A2, RINFSUP1:8; :: thesis: verum

end;

then A6: s is LowerBound of rng Eseq by XXREAL_2:def 2;
then A7: rng Eseq is bounded_below by XXREAL_2:def 9;
A8: inf (rng Eseq) <= s

proof

reconsider r1 = inf (rng Eseq) as Element of REAL by A7, A4, XXREAL_2:58;
A9: inf (rng Eseq) is LowerBound of rng Eseq by XXREAL_2:def 4;
for n being Nat holds r1 <= seq . n

proof

let n be Nat; :: thesis: r1 <= seq . n
n in NAT by ORDINAL1:def 12;
hence r1 <= seq . n by A1, A3, FUNCT_1:3, XXREAL_2:def 2, A9; :: thesis: verum

end;

hence inf (rng Eseq) <= s by RINFSUP1:10; :: thesis: verum

end;

s <= inf (rng Eseq) by A6, XXREAL_2:def 4;
hence lower_bound seq = inf (rng Eseq) by A8, XXREAL_0:1; :: thesis: verum