let L be ExtREAL_sequence; :: thesis: for c being R_eal st ( for n being Nat holds L . n = c ) holds
( L is convergent & lim L = c & lim L = sup (rng L) )
let c be R_eal; :: thesis: ( ( for n being Nat holds L . n = c ) implies ( L is convergent & lim L = c & lim L = sup (rng L) ) )
assume A1: for n being Nat holds L . n = c ; :: thesis: ( L is convergent & lim L = c & lim L = sup (rng L) )
A2: ( c in REAL or c in {-infty ,+infty } ) by XBOOLE_0:def 3, XXREAL_0:def 4;

now

let v be ext-real number ; :: thesis: ( v in rng L implies v <= c )
assume v in rng L ; :: thesis: v <= c
then consider n being set such that
A3: n in dom L and
A4: v = L . n by FUNCT_1:def 5;
n is Nat by A3;
hence v <= c by A1, A4; :: thesis: verum

end;

then A5: c is UpperBound of rng L by XXREAL_2:def 1;
( 1 in NAT & dom L = NAT ) by FUNCT_2:def 1;
then A6: ( L . 1 = c & L . 1 in rng L ) by A1, FUNCT_1:12;

per cases ( c in REAL or c = -infty or c = +infty ) by A2, TARSKI:def 2;

suppose c in REAL ; :: thesis: ( L is convergent & lim L = c & lim L = sup (rng L) )

then reconsider rc = c as real number ;

A7: now

let p be real number ; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (R_EAL rc)).| < p )
assume A8: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (R_EAL rc)).| < p

now

let m be Nat; :: thesis: ( 0 <= m implies |.((L . m) - (R_EAL rc)).| < p )
assume 0 <= m ; :: thesis: |.((L . m) - (R_EAL rc)).| < p
(L . m) - (R_EAL rc) = (L . m) + (- (L . m)) by A1;
then (L . m) - (R_EAL rc) = 0 by EXTREAL1:9;
hence |.((L . m) - (R_EAL rc)).| < p by A8, EXTREAL2:53; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (R_EAL rc)).| < p ; :: thesis: verum

end;

then A9: L is convergent_to_finite_number by Def8;
hence L is convergent by Def11; :: thesis: ( lim L = c & lim L = sup (rng L) )
hence lim L = c by A7, A9, Def12; :: thesis: lim L = sup (rng L)
hence lim L = sup (rng L) by A5, A6, XXREAL_2:55; :: thesis: verum

end;

suppose A10: c = -infty ; :: thesis: ( L is convergent & lim L = c & lim L = sup (rng L) )

for p being real number 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 number ; :: thesis: ( p < 0 implies ex n being Nat st
for m being Nat st n <= m holds
L . m <= p )
assume p < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
L . m <= p
A11: p in REAL by XREAL_0:def 1;
take 0 ; :: thesis: for m being Nat st 0 <= m holds
L . m <= p

now

let m be Nat; :: thesis: ( 0 <= m implies L . m < p )
assume 0 <= m ; :: thesis: L . m < p
L . m = -infty by A1, A10;
hence L . m < p by A11, XXREAL_0:12; :: thesis: verum

end;

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

end;

then A12: L is convergent_to_-infty by Def10;
hence L is convergent by Def11; :: thesis: ( lim L = c & lim L = sup (rng L) )
hence lim L = c by A10, A12, Def12; :: thesis: lim L = sup (rng L)
hence lim L = sup (rng L) by A5, A6, XXREAL_2:55; :: thesis: verum

end;

suppose A13: c = +infty ; :: thesis: ( L is convergent & lim L = c & lim L = sup (rng L) )

for p being real number 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 number ; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
p <= L . m )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
p <= L . m
A14: p in REAL by XREAL_0:def 1;
take 0 ; :: thesis: for m being Nat st 0 <= m holds
p <= L . m

now

let m be Nat; :: thesis: ( 0 <= m implies p < L . m )
assume 0 <= m ; :: thesis: p < L . m
L . m = +infty by A1, A13;
hence p < L . m by A14, XXREAL_0:9; :: thesis: verum

end;

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

end;

then A15: L is convergent_to_+infty by Def9;
hence L is convergent by Def11; :: thesis: ( lim L = c & lim L = sup (rng L) )
hence lim L = c by A13, A15, Def12; :: thesis: lim L = sup (rng L)
hence lim L = sup (rng L) by A5, A6, XXREAL_2:55; :: thesis: verum

end;

end;