let L be ExtREAL_sequence; :: thesis: ( ( for n, m being Nat st n <= m holds
L . n <= L . m ) implies ( L is convergent & lim L = sup (rng L) ) )
assume A1: for n, m being Nat st n <= m holds
L . n <= L . m ; :: thesis: ( L is convergent & lim L = sup (rng L) )

A2: now :: thesis: for n being Nat holds L . n <= sup (rng L)

let n be Nat; :: thesis: L . n <= sup (rng L)
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
dom L = NAT by FUNCT_2:def 1;
then A3: L . n1 in rng L by FUNCT_1:def 3;
sup (rng L) is UpperBound of rng L by XXREAL_2:def 3;
hence L . n <= sup (rng L) by A3, XXREAL_2:def 1; :: thesis: verum

end;

per cases ( for k0 being Nat holds not -infty < L . k0 or ex k0 being Nat st -infty < L . k0 ) ;

suppose A4: for k0 being Nat holds not -infty < L . k0 ; :: thesis: ( L is convergent & lim L = sup (rng L) )

now :: thesis: for x being ExtReal st x in rng L holds
x <= -infty

let x be ExtReal; :: thesis: ( x in rng L implies x <= -infty )
assume x in rng L ; :: thesis: x <= -infty
then ex n being object st
( n in dom L & x = L . n ) by FUNCT_1:def 3;
hence x <= -infty by A4; :: thesis: verum

end;

then A5: -infty is UpperBound of rng L by XXREAL_2:def 1;
for y being UpperBound of rng L holds -infty <= y by XXREAL_0:5;
then A6: -infty = sup (rng L) by A5, XXREAL_2:def 3;

now :: thesis: for K being Real st K < 0 holds
ex N0 being Nat st
for n being Nat st N0 <= n holds
L . n <= K

reconsider N0 = 0 as Nat ;
let K be Real; :: thesis: ( K < 0 implies ex N0 being Nat st
for n being Nat st N0 <= n holds
L . n <= K )
assume K < 0 ; :: thesis: ex N0 being Nat st
for n being Nat st N0 <= n holds
L . n <= K
take N0 = N0; :: thesis: for n being Nat st N0 <= n holds
L . n <= K
let n be Nat; :: thesis: ( N0 <= n implies L . n <= K )
assume N0 <= n ; :: thesis: L . n <= K
L . n = -infty by A4, XXREAL_0:6;
hence L . n <= K by XXREAL_0:5; :: thesis: verum

end;

then A7: L is convergent_to_-infty ;
then L is convergent ;
hence ( L is convergent & lim L = sup (rng L) ) by A7, A6, Def12; :: thesis: verum

end;

suppose ex k0 being Nat st -infty < L . k0 ; :: thesis: ( L is convergent & lim L = sup (rng L) )

then consider k0 being Nat such that
A8: -infty < L . k0 ;
reconsider k0 = k0 as Element of NAT by ORDINAL1:def 12;

per cases ( ex K being Real st
for n being Nat holds L . n < K or for K being Real holds
( not 0 < K or ex n being Nat st not L . n < K ) ) ;

suppose ex K being Real st
for n being Nat holds L . n < K ; :: thesis: ( L is convergent & lim L = sup (rng L) )

then consider K being Real such that
A9: for n being Nat holds L . n < K ;

now :: thesis: for x being ExtReal st x in rng L holds
x <= K

let x be ExtReal; :: thesis: ( x in rng L implies x <= K )
assume x in rng L ; :: thesis: x <= K
then ex z being object st
( z in dom L & x = L . z ) by FUNCT_1:def 3;
hence x <= K by A9; :: thesis: verum

end;

then K is UpperBound of rng L by XXREAL_2:def 1;
then A10: sup (rng L) <= K by XXREAL_2:def 3;
K in REAL by XREAL_0:def 1;
then A11: sup (rng L) <> +infty by A10, XXREAL_0:9;
A12: sup (rng L) <> -infty by A2, A8;
then reconsider h = sup (rng L) as Element of REAL by A11, XXREAL_0:14;
A13: for p being Real st 0 < p holds
ex N0 being Nat st
for m being Nat st N0 <= m holds
|.((L . m) - (sup (rng L))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex N0 being Nat st
for m being Nat st N0 <= m holds
|.((L . m) - (sup (rng L))).| < p )
assume A14: 0 < p ; :: thesis: ex N0 being Nat st
for m being Nat st N0 <= m holds
|.((L . m) - (sup (rng L))).| < p
reconsider e = p as R_eal by XXREAL_0:def 1;
sup (rng L) in REAL by A12, A11, XXREAL_0:14;
then consider y being ExtReal such that
A15: y in rng L and
A16: (sup (rng L)) - e < y by A14, MEASURE6:6;
consider x being object such that
A17: x in dom L and
A18: y = L . x by A15, FUNCT_1:def 3;
reconsider N1 = x as Element of NAT by A17;
set N0 = max (N1,k0);
take max (N1,k0) ; :: thesis: for m being Nat st max (N1,k0) <= m holds
|.((L . m) - (sup (rng L))).| < p

hereby :: thesis: verum

let n be Nat; :: thesis: ( max (N1,k0) <= n implies |.((L . n) - (sup (rng L))).| < p )
A19: N1 <= max (N1,k0) by XXREAL_0:25;
assume max (N1,k0) <= n ; :: thesis: |.((L . n) - (sup (rng L))).| < p
then N1 <= n by A19, XXREAL_0:2;
then L . N1 <= L . n by A1;
then (sup (rng L)) - e < L . n by A16, A18, XXREAL_0:2;
then sup (rng L) < (L . n) + e by XXREAL_3:54;
then (sup (rng L)) - (L . n) < e by XXREAL_3:55;
then - e < - ((sup (rng L)) - (L . n)) by XXREAL_3:38;
then A20: - e < (L . n) - (sup (rng L)) by XXREAL_3:26;
A21: L . n <= sup (rng L) by A2;

A22: now :: thesis: not sup (rng L) = (sup (rng L)) + e

assume A23: sup (rng L) = (sup (rng L)) + e ; :: thesis: contradiction
(e + (sup (rng L))) + (- (sup (rng L))) = e + ((sup (rng L)) + (- (sup (rng L)))) by A12, A11, XXREAL_3:29
.= e + 0 by XXREAL_3:7
.= e by XXREAL_3:4 ;
hence contradiction by A14, A23, XXREAL_3:7; :: thesis: verum

end;

(sup (rng L)) + 0 <= (sup (rng L)) + e by A14, XXREAL_3:36;
then sup (rng L) <= (sup (rng L)) + e by XXREAL_3:4;
then sup (rng L) < (sup (rng L)) + e by A22, XXREAL_0:1;
then L . n < (sup (rng L)) + e by A21, XXREAL_0:2;
then (L . n) - (sup (rng L)) < e by XXREAL_3:55;
hence |.((L . n) - (sup (rng L))).| < p by A20, EXTREAL1:22; :: thesis: verum

end;

end;

A24: h = sup (rng L) ;
then A25: L is convergent_to_finite_number by A13;
hence L is convergent ; :: thesis: lim L = sup (rng L)
hence lim L = sup (rng L) by A13, A24, A25, Def12; :: thesis: verum

end;

suppose A26: for K being Real holds
( not 0 < K or ex n being Nat st not L . n < K ) ; :: thesis: ( L is convergent & lim L = sup (rng L) )

now :: thesis: for K being Real st 0 < K holds
ex N0 being Nat st
for n being Nat st N0 <= n holds
K <= L . n

let K be Real; :: thesis: ( 0 < K implies ex N0 being Nat st
for n being Nat st N0 <= n holds
K <= L . n )
assume 0 < K ; :: thesis: ex N0 being Nat st
for n being Nat st N0 <= n holds
K <= L . n
then consider N0 being Nat such that
A27: K <= L . N0 by A26;

now :: thesis: for n being Nat st N0 <= n holds
K <= L . n

let n be Nat; :: thesis: ( N0 <= n implies K <= L . n )
assume N0 <= n ; :: thesis: K <= L . n
then L . N0 <= L . n by A1;
hence K <= L . n by A27, XXREAL_0:2; :: thesis: verum

end;

hence ex N0 being Nat st
for n being Nat st N0 <= n holds
K <= L . n ; :: thesis: verum

end;

then A28: L is convergent_to_+infty ;
hence A29: L is convergent ; :: thesis: lim L = sup (rng L)

now :: thesis: not sup (rng L) <> +infty

assume A30: sup (rng L) <> +infty ; :: thesis: contradiction
L . k0 <= sup (rng L) by A2;
then reconsider h = sup (rng L) as Element of REAL by A8, A30, XXREAL_0:14;
set K = max (0,h);
0 <= max (0,h) by XXREAL_0:25;
then consider N0 being Nat such that
A31: (max (0,h)) + 1 <= L . N0 by A26;
h + 0 < (max (0,h)) + 1 by XREAL_1:8, XXREAL_0:25;
then sup (rng L) < L . N0 by A31, XXREAL_0:2;
hence contradiction by A2; :: thesis: verum

end;

hence lim L = sup (rng L) by A28, A29, Def12; :: thesis: verum

end;

end;

end;

end;