let seq be ExtREAL_sequence; :: thesis: for rseq being Real_Sequence st seq = rseq & seq is convergent_to_finite_number holds
( rseq is convergent & lim seq = lim rseq )
let rseq be Real_Sequence; :: thesis: ( seq = rseq & seq is convergent_to_finite_number implies ( rseq is convergent & lim seq = lim rseq ) )
assume A1: ( seq = rseq & seq is convergent_to_finite_number ) ; :: thesis: ( rseq is convergent & lim seq = lim rseq )
then A2: seq is convergent by MESFUNC5:def 11;
( ( not lim seq = +infty or not seq is convergent_to_+infty ) & ( not lim seq = -infty or not seq is convergent_to_-infty ) ) by A1, MESFUNC5:56, MESFUNC5:57;
then consider g being real number such that
A3: ( lim seq = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) & seq is convergent_to_finite_number ) by A2, MESFUNC5:def 12;
A4: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - g) < p

proof

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - g) < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - g) < p
then consider n being Nat such that
A5: for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p by A3;
reconsider N = n as Element of NAT by ORDINAL1:def 13;
take N ; :: thesis: for m being Element of NAT st N <= m holds
abs ((rseq . m) - g) < p

hereby :: thesis: verum

let m be Element of NAT ; :: thesis: ( N <= m implies abs ((rseq . m) - g) < p )
assume N <= m ; :: thesis: abs ((rseq . m) - g) < p
then A6: |.((seq . m) - (lim seq)).| < p by A5;
( rseq . m is Real & g is Real ) by XREAL_0:def 1;
then (rseq . m) - g = (seq . m) - (lim seq) by A1, A3, SUPINF_2:5;
hence abs ((rseq . m) - g) < p by A6, EXTREAL2:49; :: thesis: verum

end;

end;

then rseq is convergent by SEQ_2:def 6;
hence ( rseq is convergent & lim seq = lim rseq ) by A3, A4, SEQ_2:def 7; :: thesis: verum