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

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

let x be ext-real number ; :: thesis: ( x in rng L implies x <= -infty )
assume x in rng L ; :: thesis: x <= -infty
then ex n being set 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

reconsider N0 = 0 as Nat ;
let K be real number ; :: 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 by Def10;
then L is convergent by Def11;
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 number st
for n being Nat holds L . n < K or for K being real number holds
( not 0 < K or ex n being Nat st not L . n < K ) ) ;

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

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

now

let x be ext-real number ; :: thesis: ( x in rng L implies x <= R_EAL K )
assume x in rng L ; :: thesis: x <= R_EAL K
then ex z being set st
( z in dom L & x = L . z ) by FUNCT_1:def 3;
hence x <= R_EAL K by A9; :: thesis: verum

end;

then R_EAL K is UpperBound of rng L by XXREAL_2:def 1;
then A10: sup (rng L) <= R_EAL K by XXREAL_2:def 3;
R_EAL K is 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 Real by A11, XXREAL_0:14;
A13: for p being real number 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 number ; :: 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 Real by XREAL_0:def 1;
sup (rng L) is Real by A12, A11, XXREAL_0:14;
then consider y being ext-real number such that
A15: y in rng L and
A16: (sup (rng L)) - (R_EAL e) < y by A14, MEASURE6:6;
consider x being set 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)) - (R_EAL e) < L . n by A16, A18, XXREAL_0:2;
then sup (rng L) < (L . n) + (R_EAL e) by XXREAL_3:54;
then (sup (rng L)) - (L . n) < R_EAL e by XXREAL_3:55;
then - (R_EAL e) < - ((sup (rng L)) - (L . n)) by XXREAL_3:38;
then A20: - (R_EAL e) < (L . n) - (sup (rng L)) by XXREAL_3:26;
A21: L . n <= sup (rng L) by A2;

A22: now

assume A23: sup (rng L) = (sup (rng L)) + e ; :: thesis: contradiction
((R_EAL e) + (sup (rng L))) + (- (sup (rng L))) = (R_EAL e) + ((sup (rng L)) + (- (sup (rng L)))) by A12, A11, XXREAL_3:29
.= (R_EAL 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)) + (R_EAL 0) <= (sup (rng L)) + (R_EAL e) by A14, XXREAL_3:36;
then sup (rng L) <= (sup (rng L)) + (R_EAL e) by XXREAL_3:4;
then sup (rng L) < (sup (rng L)) + e by A22, XXREAL_0:1;
then L . n < (sup (rng L)) + (R_EAL e) by A21, XXREAL_0:2;
then (L . n) - (sup (rng L)) < R_EAL e by XXREAL_3:55;
hence |.((L . n) - (sup (rng L))).| < p by A20, EXTREAL2:11; :: thesis: verum

end;

end;

A24: R_EAL h = sup (rng L) ;
then A25: L is convergent_to_finite_number by A13, Def8;
hence L is convergent by Def11; :: 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 number holds
( not 0 < K or ex n being Nat st not L . n < K ) ; :: thesis: ( L is convergent & lim L = sup (rng L) )

now

let K be real number ; :: 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: R_EAL K <= L . N0 by A26;

now

let n be Nat; :: thesis: ( N0 <= n implies R_EAL K <= L . n )
assume N0 <= n ; :: thesis: R_EAL K <= L . n
then L . N0 <= L . n by A1;
hence R_EAL 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 by Def9;
hence A29: L is convergent by Def11; :: thesis: lim L = sup (rng L)

now

assume A30: sup (rng L) <> +infty ; :: thesis: contradiction
L . k0 <= sup (rng L) by A2;
then reconsider h = sup (rng L) as 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: R_EAL ((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;