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