let seq be ExtREAL_sequence; :: thesis:
set a = lim_inf seq;
thus ( seq is convergent implies lim_inf seq = lim_sup seq ) :: thesis:

proof

assume A1: seq is convergent ; :: thesis:

per cases by A1, MESFUNC5:def 11;

suppose A2: seq is convergent_to_finite_number ; :: thesis:

then consider k being Nat such that
A3: seq ^\ k is bounded by Th19;
reconsider rseq0 = seq ^\ k as Real_Sequence by A3, Th11;
A4: k in NAT by ORDINAL1:def 12;
seq ^\ k is convergent_to_finite_number by A2, Th20;
then A5: rseq0 is convergent by Th15;
then A6: rseq0 is bounded ;
then lim_sup rseq0 = lim_sup (seq ^\ k) by Th9;
then A7: lim_sup rseq0 = lim_sup seq by Th28, A4;
lim_inf rseq0 = lim_inf (seq ^\ k) by A6, Th10;
then lim_inf rseq0 = lim_inf seq by Th29, A4;
hence lim_inf seq = lim_sup seq by A5, A7, RINFSUP1:88; :: thesis:

end;

suppose A8: seq is convergent_to_-infty ; :: thesis:

now :: thesis:

let g be Real; :: thesis:
assume g < 0 ; :: thesis:
then consider n being Nat such that
A9: for m being Nat st n <= m holds
seq . m <= g by A8, MESFUNC5:def 10;

now :: thesis:

let m be Nat; :: thesis:
A10: (inferior_realsequence seq) . m <= seq . m by Th8;
assume n <= m ; :: thesis:
then seq . m <= g by A9;
hence (inferior_realsequence seq) . m <= g by A10, XXREAL_0:2; :: thesis:

end;

hence ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g ; :: thesis:

end;

then A11: inferior_realsequence seq is convergent_to_-infty by MESFUNC5:def 10;
then inferior_realsequence seq is convergent by MESFUNC5:def 11;
then lim (inferior_realsequence seq) = -infty by A11, MESFUNC5:def 12;
then A12: lim_inf seq = -infty by Th37;
A13: superior_realsequence seq is convergent_to_-infty

proof

set iseq = superior_realsequence seq;
assume not superior_realsequence seq is convergent_to_-infty ; :: thesis:
then consider g being Real such that
A14: g < 0 and
A15: for n being Nat ex m being Nat st
( n <= m & g < (superior_realsequence seq) . m ) by MESFUNC5:def 10;
consider N being Nat such that
A16: for m being Nat st N <= m holds
seq . m <= g by A8, A14, MESFUNC5:def 10;

now :: thesis:

let m be Nat; :: thesis:
consider Y being non empty Subset of ExtREAL such that
A17: Y = { (seq . k) where k is Nat : m <= k } and
A18: (superior_realsequence seq) . m = sup Y by Def7;
assume A19: N <= m ; :: thesis:

now :: thesis:

let x be ExtReal; :: thesis:
assume x in Y ; :: thesis:
then consider k being Nat such that
A20: x = seq . k and
A21: m <= k by A17;
N <= k by A19, A21, XXREAL_0:2;
hence x <= g by A16, A20; :: thesis:

end;

then g is UpperBound of Y by XXREAL_2:def 1;
hence (superior_realsequence seq) . m <= g by A18, XXREAL_2:def 3; :: thesis:

end;

hence contradiction by A15; :: thesis:

end;

then superior_realsequence seq is convergent by MESFUNC5:def 11;
then lim (superior_realsequence seq) = -infty by A13, MESFUNC5:def 12;
hence lim_inf seq = lim_sup seq by A12, Th36; :: thesis:

end;

suppose A22: seq is convergent_to_+infty ; :: thesis:

now :: thesis:

let g be Real; :: thesis:
assume 0 < g ; :: thesis:
then consider n being Nat such that
A23: for m being Nat st n <= m holds
g <= seq . m by A22, MESFUNC5:def 9;

now :: thesis:

let m be Nat; :: thesis:
A24: seq . m <= (superior_realsequence seq) . m by Th8;
assume n <= m ; :: thesis:
then g <= seq . m by A23;
hence g <= (superior_realsequence seq) . m by A24, XXREAL_0:2; :: thesis:

end;

hence ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m ; :: thesis:

end;

then A25: superior_realsequence seq is convergent_to_+infty by MESFUNC5:def 9;
then superior_realsequence seq is convergent by MESFUNC5:def 11;
then lim (superior_realsequence seq) = +infty by A25, MESFUNC5:def 12;
then A26: lim_sup seq = +infty by Th36;
A27: inferior_realsequence seq is convergent_to_+infty

proof

set iseq = inferior_realsequence seq;
assume not inferior_realsequence seq is convergent_to_+infty ; :: thesis:
then consider g being Real such that
A28: 0 < g and
A29: for n being Nat ex m being Nat st
( n <= m & (inferior_realsequence seq) . m < g ) by MESFUNC5:def 9;
consider N being Nat such that
A30: for m being Nat st N <= m holds
g <= seq . m by A22, A28, MESFUNC5:def 9;

now :: thesis:

let m be Nat; :: thesis:
consider Y being non empty Subset of ExtREAL such that
A31: Y = { (seq . k) where k is Nat : m <= k } and
A32: (inferior_realsequence seq) . m = inf Y by Def6;
assume A33: N <= m ; :: thesis:

now :: thesis:

let x be ExtReal; :: thesis:
assume x in Y ; :: thesis:
then consider k being Nat such that
A34: x = seq . k and
A35: m <= k by A31;
N <= k by A33, A35, XXREAL_0:2;
hence g <= x by A30, A34; :: thesis:

end;

then g is LowerBound of Y by XXREAL_2:def 2;
hence g <= (inferior_realsequence seq) . m by A32, XXREAL_2:def 4; :: thesis:

end;

hence contradiction by A29; :: thesis:

end;

then inferior_realsequence seq is convergent by MESFUNC5:def 11;
then lim (inferior_realsequence seq) = +infty by A27, MESFUNC5:def 12;
hence lim_inf seq = lim_sup seq by A26, Th37; :: thesis:

end;

assume A36: lim_inf seq = lim_sup seq ; :: thesis:

per cases by XXREAL_0:14;

suppose lim_inf seq in REAL ; :: thesis:

hence seq is convergent by A36, Lm7; :: thesis:

end;

suppose lim_inf seq = +infty ; :: thesis:

hence seq is convergent by A36, Lm5; :: thesis:

end;

suppose lim_inf seq = -infty ; :: thesis:

hence seq is convergent by A36, Lm6; :: thesis:

end;