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

proof

assume A1: seq is convergent ; :: thesis: lim_inf seq = lim_sup seq

per cases ( seq is convergent_to_finite_number or seq is convergent_to_-infty or seq is convergent_to_+infty ) by A1, MESFUNC5:def 11;

suppose A2: seq is convergent_to_finite_number ; :: thesis: lim_inf seq = lim_sup seq

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: verum

end;

suppose A8: seq is convergent_to_-infty ; :: thesis: lim_inf seq = lim_sup seq

now :: thesis: for g being Real st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g

let g be Real; :: thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g )
assume g < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g
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: for m being Nat st n <= m holds
(inferior_realsequence seq) . m <= g

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

end;

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

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: contradiction
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: for m being Nat st N <= m holds
(superior_realsequence seq) . m <= g

let m be Nat; :: thesis: ( N <= m implies (superior_realsequence seq) . m <= g )
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: (superior_realsequence seq) . m <= g

now :: thesis: for x being ExtReal st x in Y holds
x <= g

let x be ExtReal; :: thesis: ( x in Y implies x <= g )
assume x in Y ; :: thesis: x <= g
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: verum

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: verum

end;

hence contradiction by A15; :: thesis: verum

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: verum

end;

suppose A22: seq is convergent_to_+infty ; :: thesis: lim_inf seq = lim_sup seq

now :: thesis: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m )
assume 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m
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: for m being Nat st n <= m holds
g <= (superior_realsequence seq) . m

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

end;

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

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: contradiction
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: for m being Nat st N <= m holds
g <= (inferior_realsequence seq) . m

let m be Nat; :: thesis: ( N <= m implies g <= (inferior_realsequence seq) . m )
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: g <= (inferior_realsequence seq) . m

now :: thesis: for x being ExtReal st x in Y holds
g <= x

let x be ExtReal; :: thesis: ( x in Y implies g <= x )
assume x in Y ; :: thesis: g <= x
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: verum

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: verum

end;

hence contradiction by A29; :: thesis: verum

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: verum

end;

end;

end;

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

per cases ( lim_inf seq in REAL or lim_inf seq = +infty or lim_inf seq = -infty ) by XXREAL_0:14;

suppose lim_inf seq in REAL ; :: thesis: seq is convergent

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

end;

suppose lim_inf seq = +infty ; :: thesis: seq is convergent

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

end;

suppose lim_inf seq = -infty ; :: thesis: seq is convergent

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

end;

end;