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 )

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:4; :: 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, Th32;
hence A7: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = inf 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:4;
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 inf seq = +infty by XXREAL_2:13;
hence lim seq = inf seq by A6, A7, 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) by A1, Th25;

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 LowerBound of rng (seq ^\ k) by XXREAL_2:42;
hence contradiction by A9, A10, A12, XXREAL_2:56; :: thesis: verum

end;

A13: inf (seq ^\ k) <= sup (seq ^\ k) by Th24;
A14: inf (rng (seq ^\ k)) is LowerBound of rng (seq ^\ k) by XXREAL_2:def 4;
inf seq <= seq . k by Th23;
then -infty < seq . k by A9, XXREAL_0:2, XXREAL_0:6;
then A15: seq ^\ k is bounded_above by A1, A8, Th30;
then rng (seq ^\ k) is bounded_above ;
then sup (rng (seq ^\ k)) < +infty by A11, XXREAL_0:9, XXREAL_2:57;
then inf (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14;
then rng (seq ^\ k) is bounded_below by A14, XXREAL_2:def 9;
then seq ^\ k is bounded_below ;
then A16: seq ^\ k is bounded by A15;
A17: seq ^\ k is non-increasing by A1, Th25;
then A18: lim (seq ^\ k) = inf (seq ^\ k) by A16, Lm3;
seq ^\ k is convergent by A17, A16, Lm3;
hence ( seq is convergent & lim seq = inf seq ) by A10, A18, Th17; :: thesis: verum

end;

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

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

end;

end;

end;

end;