let seq be ExtREAL_sequence; :: thesis: ( lim_inf seq = lim_sup seq & lim_inf seq in REAL 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 in REAL ; :: thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
consider k being Nat such that
A3: seq ^\ k is bounded by A1, A2, Th18;
reconsider rseq0 = seq ^\ k as Real_Sequence by ;
seq ^\ k is bounded_below by A3;
then A4: rseq0 is V71() by Th13;
A5: k in NAT by ORDINAL1:def 12;
seq ^\ k is bounded_above by A3;
then A6: rseq0 is V70() by Th12;
then lim_sup rseq0 = lim_sup (seq ^\ k) by ;
then A7: lim_sup rseq0 = lim_sup seq by ;
lim_inf rseq0 = lim_inf (seq ^\ k) by A6, A4, Th10;
then A8: lim_inf rseq0 = lim_inf seq by ;
then A9: rseq0 is convergent by ;
then A10: lim rseq0 = lim_inf seq by ;
A11: seq ^\ k is convergent by ;
A12: lim rseq0 = lim (seq ^\ k) by ;
lim rseq0 = lim_sup seq by ;
hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by ; :: thesis: verum