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;
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
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;
now :: thesis: for m being Nat st n <= m holds
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;
hence ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m ; :: thesis: verum
end;
then A6: seq is convergent_to_+infty by MESFUNC5:def 9;
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