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: inferior_realsequence seq is convergent_to_+infty by A2, Th35;

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: inferior_realsequence seq is convergent_to_+infty by A2, Th35;

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

ex n being Nat st

for m being Nat st n <= m holds

g <= seq . m

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

for m being Nat st n <= m holds

g <= seq . m

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

for m being Nat st n <= m holds

g <= seq . m )

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

for m being Nat st n <= m holds

g <= seq . m

then consider n being Nat such that

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

g <= (inferior_realsequence seq) . m by A3, MESFUNC5:def 9;

for m being Nat st n <= m holds

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

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

g <= seq . m )

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

for m being Nat st n <= m holds

g <= seq . m

then consider n being Nat such that

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

g <= (inferior_realsequence seq) . m by A3, MESFUNC5:def 9;

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

g <= seq . m

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

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

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

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

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

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

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

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

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

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

for m being Nat st n <= m holds

g <= seq . m ; :: 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