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

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

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

then A3: seq is convergent_to_+infty by Th32;
hence A4: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = inf 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:4;
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:4; :: 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 inf seq = +infty by XXREAL_2:13;
hence lim seq = inf seq by A3, A4, MESFUNC5:def 12; :: thesis: verum

end;

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

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

per cases ( -infty <> inf seq or -infty = inf seq ) ;

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

set seq0 = seq ^\ k;
A10: ( inf seq = inf (seq ^\ k) & seq ^\ k is non-increasing ) by A1, Th25;
inf seq <= seq . k by Th23;
then -infty < seq . k by A9, XXREAL_0:2, XXREAL_0:6;
then A11: seq ^\ k is bounded_above by A1, A8, Th30;
then A12: rng (seq ^\ k) is bounded_above by Def4;

now

assume A13: rng (seq ^\ k) = {-infty } ; :: thesis: contradiction
A14: -infty is LowerBound of rng (seq ^\ k) by XXREAL_2:42;
-infty in rng (seq ^\ k) by A13, TARSKI:def 1;
hence contradiction by A9, A10, A14, XXREAL_2:56; :: thesis: verum

end;

then A15: sup (rng (seq ^\ k)) < +infty by A12, XXREAL_0:9, XXREAL_2:57;
inf (seq ^\ k) <= sup (seq ^\ k) by Th24;
then A16: inf (rng (seq ^\ k)) in REAL by A9, A10, A15, XXREAL_0:14;
inf (rng (seq ^\ k)) is LowerBound of rng (seq ^\ k) by XXREAL_2:def 4;
then rng (seq ^\ k) is bounded_below by A16, SUPINF_1:def 12;
then seq ^\ k is bounded_below by Def3;
then seq ^\ k is bounded by A11, Def5;
then ( seq ^\ k is convergent & lim (seq ^\ k) = inf (seq ^\ k) ) by A10, Lm4;
hence ( seq is convergent & lim seq = inf seq ) by A10, Th17; :: thesis: verum

end;

suppose A17: -infty = inf seq ; :: thesis: ( seq is convergent & lim seq = inf seq )

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

end;

end;

end;

end;