let seq be ExtREAL_sequence; :: thesis: ( lim_inf seq = lim_sup seq & lim_inf seq = -infty implies ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) )

assume that

A1: lim_inf seq = lim_sup seq and

A2: lim_inf seq = -infty ; :: thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )

A3: superior_realsequence seq is convergent_to_-infty by A1, A2, Th34;

then seq is convergent by MESFUNC5:def 11;

hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, A2, A6, MESFUNC5:def 12; :: thesis: verum

assume that

A1: lim_inf seq = lim_sup seq and

A2: lim_inf seq = -infty ; :: thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )

A3: superior_realsequence seq is convergent_to_-infty by A1, A2, Th34;

now :: thesis: for g being Real st g < 0 holds

ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g

then A6:
seq is convergent_to_-infty
by MESFUNC5:def 10;ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g

let g be Real; :: thesis: ( g < 0 implies ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g )

assume g < 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g

then consider n being Nat such that

A4: for m being Nat st n <= m holds

(superior_realsequence seq) . m <= g by A3, MESFUNC5:def 10;

for m being Nat st n <= m holds

seq . m <= g ; :: thesis: verum

end;for m being Nat st n <= m holds

seq . m <= g )

assume g < 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g

then consider n being Nat such that

A4: for m being Nat st n <= m holds

(superior_realsequence seq) . m <= g by A3, MESFUNC5:def 10;

now :: thesis: for m being Nat st n <= m holds

seq . m <= g

hence
ex n being Nat st seq . m <= g

let m be Nat; :: thesis: ( n <= m implies seq . m <= g )

A5: seq . m <= (superior_realsequence seq) . m by Th8;

assume n <= m ; :: thesis: seq . m <= g

then (superior_realsequence seq) . m <= g by A4;

hence seq . m <= g by A5, XXREAL_0:2; :: thesis: verum

end;A5: seq . m <= (superior_realsequence seq) . m by Th8;

assume n <= m ; :: thesis: seq . m <= g

then (superior_realsequence seq) . m <= g by A4;

hence seq . m <= g by A5, XXREAL_0:2; :: thesis: verum

for m being Nat st n <= m holds

seq . m <= g ; :: thesis: verum

then seq is convergent by MESFUNC5:def 11;

hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, A2, A6, MESFUNC5:def 12; :: thesis: verum