let L be ExtREAL_sequence; :: thesis:
let c be ExtReal; :: thesis:
reconsider cc = c as R_eal by XXREAL_0:def 1;
A1: dom L = NAT by FUNCT_2:def 1;
c in ExtREAL by XXREAL_0:def 1;
then A2: ( c in REAL or c in {-infty,+infty} ) by XBOOLE_0:def 3, XXREAL_0:def 4;
assume A3: for n being Nat holds L . n = c ; :: thesis:
then A4: L . 1 = c ;

now :: thesis:

let v be ExtReal; :: thesis:
assume v in rng L ; :: thesis:
then ex n being object st
( n in dom L & v = L . n ) by FUNCT_1:def 3;
hence v <= c by A3; :: thesis:

end;

then A5: c is UpperBound of rng L by XXREAL_2:def 1;

per cases by A2, TARSKI:def 2;

suppose c in REAL ; :: thesis:

then reconsider rc = c as Real ;

A6: now :: thesis:

reconsider n = 0 as Nat ;
let p be Real; :: thesis:
assume A7: 0 < p ; :: thesis:
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
(L . m) - rc = (L . m) - (L . m) by A3;
then (L . m) - rc = 0 by XXREAL_3:7;
hence |.((L . m) - rc).| < p by A7, EXTREAL1:16; :: thesis:

end;

then A8: L is convergent_to_finite_number ;
hence L is convergent ; :: thesis:
then lim L = cc by A6, A8, Def12;
hence lim L = c ; :: thesis:
hence lim L = sup (rng L) by A5, A1, A4, FUNCT_1:3, XXREAL_2:55; :: thesis:

end;

suppose A9: c = -infty ; :: thesis:

for p being Real st p < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
L . m <= p

proof

let p be Real; :: thesis:
assume p < 0 ; :: thesis:
take 0 ; :: thesis:
A10: p in REAL by XREAL_0:def 1;

now :: thesis:

let m be Nat; :: thesis:
assume 0 <= m ; :: thesis:
L . m = -infty by A3, A9;
hence L . m < p by A10, XXREAL_0:12; :: thesis:

end;

hence for m being Nat st 0 <= m holds
L . m <= p ; :: thesis:

end;

then A11: L is convergent_to_-infty ;
hence L is convergent ; :: thesis:
hence lim L = c by A9, A11, Def12; :: thesis:
hence lim L = sup (rng L) by A5, A1, A4, FUNCT_1:3, XXREAL_2:55; :: thesis:

end;

suppose A12: c = +infty ; :: thesis:

for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
p <= L . m

proof

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
take 0 ; :: thesis:
A13: p in REAL by XREAL_0:def 1;

now :: thesis:

let m be Nat; :: thesis:
assume 0 <= m ; :: thesis:
L . m = +infty by A3, A12;
hence p < L . m by A13, XXREAL_0:9; :: thesis:

end;

hence for m being Nat st 0 <= m holds
p <= L . m ; :: thesis:

end;

then A14: L is convergent_to_+infty ;
hence L is convergent ; :: thesis:
hence lim L = c by A12, A14, Def12; :: thesis:
hence lim L = sup (rng L) by A5, A1, A4, FUNCT_1:3, XXREAL_2:55; :: thesis:

end;

end;