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 A3, Th11;

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 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; :: thesis: verum

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 A3, Th11;

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 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; :: thesis: verum