let seq be Function of NAT ,REAL ; :: thesis: for Eseq being Function of NAT ,ExtREAL st seq = Eseq & seq is bounded_below holds
inf seq = inf (rng Eseq)
let Eseq be Function of NAT ,ExtREAL ; :: thesis: ( seq = Eseq & seq is bounded_below implies inf seq = inf (rng Eseq) )
assume A1: ( seq = Eseq & seq is bounded_below ) ; :: thesis: inf seq = inf (rng Eseq)
A2: ( dom Eseq = NAT & dom seq = NAT ) by FUNCT_2:def 1;
reconsider s = inf seq as R_eal by XXREAL_0:def 1;
for x being ext-real number st x in rng Eseq holds
s <= x

proof

let x be ext-real number ; :: thesis: ( x in rng Eseq implies s <= x )
assume x in rng Eseq ; :: thesis: s <= x
then consider n1 being set such that
A3: ( n1 in NAT & Eseq . n1 = x ) by A2, FUNCT_1:def 5;
thus s <= x by A1, A3, RINFSUP1:8; :: thesis: verum

end;

then A4: s is LowerBound of rng Eseq by XXREAL_2:def 2;
then A5: rng Eseq is bounded_below by SUPINF_1:def 12;
A6: 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 set such that
A7: ( n1 in NAT & Eseq . n1 = k1 ) by A2, FUNCT_1:def 5;
reconsider n1 = n1 as Element of NAT by A7;
seq . n1 = k1 by A1;
hence contradiction ; :: thesis: verum

end;

A9: s <= inf (rng Eseq) by A4, XXREAL_2:def 4;
inf (rng Eseq) <= s

proof

A10: inf (rng Eseq) is LowerBound of rng Eseq by XXREAL_2:def 4;
reconsider r1 = inf (rng Eseq) as Real by A5, A6, XXREAL_2:58;
for n being Element of NAT holds r1 <= seq . n by A1, A2, A10, FUNCT_1:12, XXREAL_2:def 2;
hence inf (rng Eseq) <= s by RINFSUP1:10; :: thesis: verum

end;

hence inf seq = inf (rng Eseq) by A9, XXREAL_0:1; :: thesis: verum