let seq be Real_Sequence; :: thesis: for seq1 being sequence of RNS_Real st seq = seq1 & seq is convergent holds
lim seq = lim seq1
let seq1 be sequence of RNS_Real; :: thesis: ( seq = seq1 & seq is convergent implies lim seq = lim seq1 )
assume AS: seq = seq1 ; :: thesis: ( not seq is convergent or lim seq = lim seq1 )
assume P1: seq is convergent ; :: thesis: lim seq = lim seq1
then P5: seq1 is convergent by AS, RNS8;
reconsider s1 = lim seq as Point of RNS_Real by XREAL_0:def 1;

now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq1 . m) - s1).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
||.((seq1 . m) - s1).|| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((seq1 . m) - s1).|| < p
then consider n being Nat such that
P2: for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p by P1, SEQ_2:def 7;
take n = n; :: thesis: for m being Nat st n <= m holds
||.((seq1 . m) - s1).|| < p

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies ||.((seq1 . m) - s1).|| < p )
assume n <= m ; :: thesis: ||.((seq1 . m) - s1).|| < p
then P3: |.((seq . m) - (lim seq)).| < p by P2;
(seq . m) - (lim seq) = (seq1 . m) - s1 by AS, RNS4;
hence ||.((seq1 . m) - s1).|| < p by P3, EUCLID:def 2; :: thesis: verum

end;

end;

hence lim seq1 = lim seq by P5, NORMSP_1:def 7; :: thesis: verum