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 that
A1: seq = rseq and
A2: seq is convergent_to_finite_number ; :: thesis: ( rseq is convergent & lim seq = lim rseq )
A3: ( not lim seq = +infty or not seq is convergent_to_+infty ) by ;
A4: ( not lim seq = -infty or not seq is convergent_to_-infty ) by ;
seq is convergent by ;
then consider g being Real such that
A5: lim seq = g and
A6: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p and
seq is convergent_to_finite_number by ;
A7: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((rseq . m) - g).| < p
proof
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((rseq . m) - g).| < p )

assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((rseq . m) - g).| < p

then consider n being Nat such that
A8: for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p by A6;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
take N ; :: thesis: for m being Nat st N <= m holds
|.((rseq . m) - g).| < p

hereby :: thesis: verum
let m be Nat; :: thesis: ( N <= m implies |.((rseq . m) - g).| < p )
assume N <= m ; :: thesis: |.((rseq . m) - g).| < p
then A9: |.((seq . m) - (lim seq)).| < p by A8;
(rseq . m) - g = (seq . m) - (lim seq) by ;
hence |.((rseq . m) - g).| < p by ; :: thesis: verum
end;
end;
then rseq is convergent by SEQ_2:def 6;
hence ( rseq is convergent & lim seq = lim rseq ) by ; :: thesis: verum