let seq be ExtREAL_sequence; :: thesis: ( seq is non-decreasing implies ( seq is convergent & lim seq = sup seq ) )
assume A1: seq is non-decreasing ; :: thesis: ( seq is convergent & lim seq = sup seq )

per cases ( for n being Element of NAT holds seq . n <= -infty or ex n being Element of NAT st not seq . n <= -infty ) ;

suppose A2: for n being Element of NAT holds seq . n <= -infty ; :: thesis: ( seq is convergent & lim seq = sup seq )

now :: thesis: for y being object st y in {-infty} holds
y in rng seq

let y be object ; :: thesis: ( y in {-infty} implies y in rng seq )
assume y in {-infty} ; :: thesis: y in rng seq
then A3: y = -infty by TARSKI:def 1;

now :: thesis: y in rng seq

assume A4: not y in rng seq ; :: thesis: contradiction

now :: thesis: for n being Element of NAT holds contradiction

let n be Element of NAT ; :: thesis: contradiction
n in NAT ;
then n in dom seq by FUNCT_2:def 1;
then seq . n <> -infty by A3, A4, FUNCT_1:def 3;
hence contradiction by A2, XXREAL_0:6; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

hence y in rng seq ; :: thesis: verum

end;

then A5: {-infty} c= rng seq ;
A6: seq is convergent_to_-infty by A2, Th33;
hence A7: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = sup seq

now :: thesis: for y being object st y in rng seq holds
y in {-infty}

let y be object ; :: thesis: ( y in rng seq implies y in {-infty} )
assume y in rng seq ; :: thesis: y in {-infty}
then ex x being object st
( x in dom seq & seq . x = y ) by FUNCT_1:def 3;
then y = -infty by A2, XXREAL_0:6;
hence y in {-infty} by TARSKI:def 1; :: thesis: verum

end;

then rng seq c= {-infty} ;
then rng seq = {-infty} by A5, XBOOLE_0:def 10;
then sup seq = -infty by XXREAL_2:11;
hence lim seq = sup seq by A6, A7, MESFUNC5:def 12; :: thesis: verum

end;

suppose not for n being Element of NAT holds seq . n <= -infty ; :: thesis: ( seq is convergent & lim seq = sup seq )

then consider k being Element of NAT such that
A8: -infty < seq . k ;

per cases ( +infty <> sup seq or +infty = sup seq ) ;

suppose A9: +infty <> sup seq ; :: thesis: ( seq is convergent & lim seq = sup seq )

set seq0 = seq ^\ k;
A10: sup seq = sup (seq ^\ k) by A1, Th26;

A11: now :: thesis: not rng (seq ^\ k) = {+infty}

assume rng (seq ^\ k) = {+infty} ; :: thesis: contradiction
then A12: +infty in rng (seq ^\ k) by TARSKI:def 1;
+infty is UpperBound of rng (seq ^\ k) by XXREAL_2:41;
hence contradiction by A9, A10, A12, XXREAL_2:55; :: thesis: verum

end;

A13: inf (seq ^\ k) <= sup (seq ^\ k) by Th24;
A14: sup (rng (seq ^\ k)) is UpperBound of rng (seq ^\ k) by XXREAL_2:def 3;
seq . k <= sup seq by Th23;
then seq . k < +infty by A9, XXREAL_0:2, XXREAL_0:4;
then A15: seq ^\ k is bounded_below by A1, A8, Th31;
then rng (seq ^\ k) is bounded_below ;
then -infty < inf (rng (seq ^\ k)) by A11, XXREAL_0:12, XXREAL_2:58;
then sup (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14;
then rng (seq ^\ k) is bounded_above by A14, XXREAL_2:def 10;
then seq ^\ k is bounded_above ;
then A16: seq ^\ k is bounded by A15;
A17: seq ^\ k is non-decreasing by A1, Th26;
then A18: lim (seq ^\ k) = sup (seq ^\ k) by A16, Lm4;
seq ^\ k is convergent by A17, A16, Lm4;
hence ( seq is convergent & lim seq = sup seq ) by A10, A18, Th17; :: thesis: verum

end;

suppose A19: +infty = sup seq ; :: thesis: ( seq is convergent & lim seq = sup seq )

then seq is convergent_to_+infty by A1, Th35;
hence seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = sup seq
thus lim seq = sup seq by A1, A19, Th35; :: thesis: verum

end;

end;

end;

end;