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;

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

( 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

then A6:
seq is convergent_to_finite_number
by MESFUNC5:def 8;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;

for m being Nat st N <= m holds

|.((seq . m) - lrs).| < e ; :: thesis: verum

end;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

hence
ex N being Nat st |.((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;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

for m being Nat st N <= m holds

|.((seq . m) - lrs).| < e ; :: thesis: verum

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