let seq be Function of NAT,REAL; :: thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is bounded_above holds
upper_bound seq = sup (rng Eseq)
let Eseq be Function of NAT,ExtREAL; :: thesis: ( seq = Eseq & seq is bounded_above implies upper_bound seq = sup (rng Eseq) )
assume that
A1: seq = Eseq and
A2: seq is bounded_above ; :: thesis: upper_bound seq = sup (rng Eseq)
reconsider s = upper_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 set 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 ext-real number st x in rng Eseq holds
x <= s

proof

let x be ext-real number ; :: thesis: ( x in rng Eseq implies x <= s )
assume x in rng Eseq ; :: thesis: x <= s
then ex n1 being set st
( n1 in NAT & Eseq . n1 = x ) by A3, FUNCT_1:def 3;
hence x <= s by A1, A2, RINFSUP1:7; :: thesis: verum

end;

then A6: s is UpperBound of rng Eseq by XXREAL_2:def 1;
then A7: rng Eseq is bounded_above by XXREAL_2:def 10;
A8: s <= sup (rng Eseq)

proof

reconsider r1 = sup (rng Eseq) as Real by A7, A4, XXREAL_2:57;
sup (rng Eseq) is UpperBound of rng Eseq by XXREAL_2:def 3;
then for n being Element of NAT holds seq . n <= r1 by A1, A3, FUNCT_1:3, XXREAL_2:def 1;
hence s <= sup (rng Eseq) by RINFSUP1:9; :: thesis: verum

end;

sup (rng Eseq) <= s by A6, XXREAL_2:def 3;
hence upper_bound seq = sup (rng Eseq) by A8, XXREAL_0:1; :: thesis: verum