let seq be ExtREAL_sequence; ( 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
; ( 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 A3, Th11;
seq ^\ k is bounded_below
by A3;
then A4:
rseq0 is bounded_below
by Th13;
A5:
k in NAT
by ORDINAL1:def 12;
seq ^\ k is bounded_above
by A3;
then A6:
rseq0 is bounded_above
by Th12;
then
lim_sup rseq0 = lim_sup (seq ^\ k)
by A4, Th9;
then A7:
lim_sup rseq0 = lim_sup seq
by Th28, A5;
lim_inf rseq0 = lim_inf (seq ^\ k)
by A6, A4, Th10;
then A8:
lim_inf rseq0 = lim_inf seq
by Th29, A5;
then A9:
rseq0 is convergent
by A1, A6, A4, A7, RINFSUP1:88;
then A10:
lim rseq0 = lim_inf seq
by A8, RINFSUP1:89;
A11:
seq ^\ k is convergent
by A9, Th14;
A12:
lim rseq0 = lim (seq ^\ k)
by A9, Th14;
lim rseq0 = lim_sup seq
by A7, A9, RINFSUP1:89;
hence
( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
by A10, A12, A11, Th17; verum