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 )

A3: 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
A4: for m being Element of NAT st n <= m holds
abs ((rseq . m) - (lim rseq)) < e by A2, SEQ_2:def 7;
set N = n;

now

let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - (R_EAL (lim rseq))).| < e )
A5: m is Element of NAT by ORDINAL1:def 13;
A6: (rseq . m) - (lim rseq) = (seq . m) - (R_EAL (lim rseq)) by A1, SUPINF_2:5;
assume n <= m ; :: thesis: |.((seq . m) - (R_EAL (lim rseq))).| < e
then abs ((rseq . m) - (lim rseq)) < e by A4, A5;
hence |.((seq . m) - (R_EAL (lim rseq))).| < e by A6, 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 A7: 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, A7, MESFUNC5:def 12; :: thesis: verum