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 A1: ( lim_inf seq = lim_sup seq & lim_inf seq in REAL ) ; :: thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq )
consider k being Element of NAT such that
A2: seq ^\ k is bounded by A1, Th18;
reconsider rseq0 = seq ^\ k as Real_Sequence by A2, Th11;
( seq ^\ k is bounded_above & seq ^\ k is bounded_below ) by A2, Def5;
then ( rseq0 is bounded_above & rseq0 is bounded_below ) by Th12, Th13;
then A3: rseq0 is bounded ;
then ( lim_inf rseq0 = lim_inf (seq ^\ k) & lim_sup rseq0 = lim_sup (seq ^\ k) ) by Th9, Th10;
then A4: ( lim_inf rseq0 = lim_inf seq & lim_sup rseq0 = lim_sup seq ) by Th28, Th29;
then rseq0 is convergent by A1, A3, RINFSUP1:90;
then ( lim rseq0 = lim_sup seq & lim rseq0 = lim_inf seq & lim rseq0 = lim (seq ^\ k) & seq ^\ k is convergent ) by A4, Th14, RINFSUP1:91;
hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by Th17; :: thesis: verum