let seq be sequence of REAL; :: thesis: for Eseq being sequence of ExtREAL st seq = Eseq & seq is V108() holds
upper_bound seq = sup (rng Eseq)
let Eseq be sequence of ExtREAL; :: thesis: ( seq = Eseq & seq is V108() implies upper_bound seq = sup (rng Eseq) )
assume that
A1: seq = Eseq and
A2: seq is V108() ; :: 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 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
x <= s

proof

let x be ExtReal; :: thesis: ( x in rng Eseq implies x <= s )
assume x in rng Eseq ; :: thesis: x <= s
then ex n1 being object 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 Element of REAL by A7, A4, XXREAL_2:57;
A9: sup (rng Eseq) is UpperBound of rng Eseq by XXREAL_2:def 3;
for n being Nat holds seq . n <= r1

proof

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

end;

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