let seq be ExtREAL_sequence; :: thesis: for rseq being Real_Sequence st seq = rseq & rseq is convergent holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq )
let rseq be Real_Sequence; :: thesis: ( seq = rseq & rseq is convergent implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq ) )
assume that
A1: seq = rseq and
A2: rseq is convergent ; :: thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq )
reconsider lrs = lim rseq as R_eal by XXREAL_0:def 1;

A3: now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - lrs).| < e

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - lrs).| < e )
assume 0 < e ; :: thesis: ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - lrs).| < e
then consider n being Nat such that
A4: for m being Nat st n <= m holds
|.((rseq . m) - (lim rseq)).| < e by A2, SEQ_2:def 7;
set N = n;

now :: thesis: for m being Nat st n <= m holds
|.((seq . m) - (lim rseq)).| < e

let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - (lim rseq)).| < e )
A5: (rseq . m) - (lim rseq) = (seq . m) - (lim rseq) by A1, SUPINF_2:3;
assume n <= m ; :: thesis: |.((seq . m) - (lim rseq)).| < e
then |.((rseq . m) - (lim rseq)).| < e by A4;
hence |.((seq . m) - (lim rseq)).| < e by A5, EXTREAL1:12; :: thesis: verum

end;

hence ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - lrs).| < e ; :: thesis: verum

end;

then A6: seq is convergent_to_finite_number by MESFUNC5:def 8;
then seq is convergent by MESFUNC5:def 11;
hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq ) by A3, A6, MESFUNC5:def 12; :: thesis: verum