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 A1: ( seq = rseq & rseq is convergent ) ; :: thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq )

A2: now

let e be real number ; :: thesis: ( 0 < e implies ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - (R_EAL (lim rseq))).| < e )
assume 0 < e ; :: thesis: ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - (R_EAL (lim rseq))).| < e
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
abs ((rseq . m) - (lim rseq)) < e by A1, SEQ_2:def 7;
set N = n;

now

let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - (R_EAL (lim rseq))).| < e )
assume A4: n <= m ; :: thesis: |.((seq . m) - (R_EAL (lim rseq))).| < e
m is Element of NAT by ORDINAL1:def 13;
then A5: abs ((rseq . m) - (lim rseq)) < e by A3, A4;
(rseq . m) - (lim rseq) = (seq . m) - (R_EAL (lim rseq)) by A1, SUPINF_2:5;
hence |.((seq . m) - (R_EAL (lim rseq))).| < e by A5, EXTREAL2:49; :: thesis: verum

end;

hence ex N being Nat st
for m being Nat st N <= m holds
|.((seq . m) - (R_EAL (lim rseq))).| < 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 A2, A6, MESFUNC5:def 12; :: thesis: verum