let seq be Function of NAT ,REAL ; :: thesis: for Eseq being Function of NAT ,ExtREAL st seq = Eseq & seq is bounded_above holds
sup seq = sup (rng Eseq)
let Eseq be Function of NAT ,ExtREAL ; :: thesis: ( seq = Eseq & seq is bounded_above implies sup seq = sup (rng Eseq) )
assume A1: ( seq = Eseq & seq is bounded_above ) ; :: thesis: sup seq = sup (rng Eseq)
A2: ( dom Eseq = NAT & dom seq = NAT ) by FUNCT_2:def 1;
reconsider s = sup seq as R_eal by XXREAL_0:def 1;
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 consider n1 being set such that
A3: ( n1 in NAT & Eseq . n1 = x ) by A2, FUNCT_1:def 5;
thus x <= s by A1, A3, RINFSUP1:7; :: thesis: verum

end;

then A4: s is UpperBound of rng Eseq by XXREAL_2:def 1;
then A5: rng Eseq is bounded_above by SUPINF_1:def 11;
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: sup (rng Eseq) <= s by A4, XXREAL_2:def 3;
s <= sup (rng Eseq)

proof

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

end;

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