let seq be Real_Sequence; :: thesis: for seq1 being sequence of RNS_Real st seq = seq1 holds
( seq is convergent iff seq1 is convergent )
let seq1 be sequence of RNS_Real; :: thesis: ( seq = seq1 implies ( seq is convergent iff seq1 is convergent ) )
assume AS: seq = seq1 ; :: thesis: ( seq is convergent iff seq1 is convergent )

hereby :: thesis: ( seq1 is convergent implies seq is convergent )

assume P1: seq is convergent ; :: thesis: seq1 is convergent
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 seq1 is convergent ; :: thesis: verum

end;

assume P4: seq1 is convergent ; :: thesis: seq is convergent
reconsider s1 = lim seq1 as Real ;

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

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

hereby :: thesis: verum

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

end;

end;

hence seq is convergent ; :: thesis: verum