let n be Nat; :: thesis:
let s1 be sequence of (Euclid n); :: thesis:
let s2 be sequence of (REAL-NS n); :: thesis:
assume A1: s1 = s2 ; :: thesis:

hereby :: thesis:

assume s1 is convergent ; :: thesis:
then consider x being Element of (Euclid n) such that
A2: for r being Real st r > 0 holds
ex n0 being Nat st
for m being Nat st n0 <= m holds
dist ((s1 . m),x) < r ;
x is Element of (TOP-REAL n) by EUCLID:67;
then x is Element of REAL n by EUCLID:22;
then reconsider g = x as Point of (REAL-NS n) by REAL_NS1:def 4;

now :: thesis:

take g = g; :: thesis:

hereby :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider n0 being Nat such that
A3: for m being Nat st n0 <= m holds
dist ((s1 . m),x) < r by A2;

hereby :: thesis:

take n0 = n0; :: thesis:

hereby :: thesis:

let n1 be Nat; :: thesis:
assume n0 <= n1 ; :: thesis:
then ( dist ((s1 . n1),x) < r & s1 . n1 = s2 . n1 ) by A1, A3;
hence ||.((s2 . n1) - g).|| < r by Th9; :: thesis:

end;

end;

end;

end;

hence s2 is convergent ; :: thesis:

end;

assume s2 is convergent ; :: thesis:
then consider g being Point of (REAL-NS n) such that
A4: for r being Real st 0 < r holds
ex m being Nat st
for n0 being Nat st m <= n0 holds
||.((s2 . n0) - g).|| < r ;
g is Element of REAL n by REAL_NS1:def 4;
then g is Element of (TOP-REAL n) by EUCLID:22;
then reconsider x = g as Element of (Euclid n) by EUCLID:67;

now :: thesis:

take x = x; :: thesis:

hereby :: thesis:

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider m0 being Nat such that
A5: for n0 being Nat st m0 <= n0 holds
||.((s2 . n0) - g).|| < r by A4;

hereby :: thesis:

take m0 = m0; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume m0 <= m ; :: thesis:
then ( ||.((s2 . m) - g).|| < r & s2 . m = s1 . m ) by A1, A5;
hence dist ((s1 . m),x) < r by Th9; :: thesis:

end;

end;

end;

end;

hence s1 is convergent ; :: thesis: