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 )

then A3: seq is convergent_to_-infty by Th33;
hence A4: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = sup seq
rng seq = {-infty }

proof

now

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

end;

then A5: rng seq c= {-infty } by TARSKI:def 3;

now

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

now

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

now

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 A6, A7, FUNCT_1:def 5;
hence contradiction by A2, XXREAL_0:6; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

hence y in rng seq ; :: thesis: verum

end;

then {-infty } c= rng seq by TARSKI:def 3;
hence rng seq = {-infty } by A5, XBOOLE_0:def 10; :: thesis: verum

end;

then sup seq = -infty by XXREAL_2:11;
hence lim seq = sup seq by A3, A4, 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: seq ^\ k is non-decreasing by A1, Th26;
seq . k <= sup seq by Th23;
then seq . k < +infty by A9, XXREAL_0:2, XXREAL_0:4;
then A12: seq ^\ k is bounded_below by A1, A8, Th31;
then A13: rng (seq ^\ k) is bounded_below by Def3;

now

assume rng (seq ^\ k) = {+infty } ; :: thesis: contradiction
then A14: +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, A14, XXREAL_2:55; :: thesis: verum

end;

then A15: -infty < inf (rng (seq ^\ k)) by A13, XXREAL_0:12, XXREAL_2:58;
inf (seq ^\ k) <= sup (seq ^\ k) by Th24;
then A16: sup (rng (seq ^\ k)) in REAL by A9, A10, A15, XXREAL_0:14;
sup (rng (seq ^\ k)) is UpperBound of rng (seq ^\ k) by XXREAL_2:def 3;
then rng (seq ^\ k) is bounded_above by A16, SUPINF_1:def 11;
then seq ^\ k is bounded_above by Def4;
then seq ^\ k is bounded by A12, Def5;
then ( seq ^\ k is convergent & lim (seq ^\ k) = sup (seq ^\ k) ) by A11, Lm5;
hence ( seq is convergent & lim seq = sup seq ) by A10, Th17; :: thesis: verum

end;

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

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

end;

end;

end;

end;