let n be Nat; :: thesis: for s1 being sequence of (Euclid n)
for s2 being sequence of (REAL-NS n) st s1 = s2 holds
( s1 is convergent iff s2 is convergent )
let s1 be sequence of (Euclid n); :: thesis: for s2 being sequence of (REAL-NS n) st s1 = s2 holds
( s1 is convergent iff s2 is convergent )
let s2 be sequence of (REAL-NS n); :: thesis: ( s1 = s2 implies ( s1 is convergent iff s2 is convergent ) )
assume A1: s1 = s2 ; :: thesis: ( s1 is convergent iff s2 is convergent )

hereby :: thesis: ( s2 is convergent implies s1 is convergent )

assume s1 is convergent ; :: thesis: s2 is convergent
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: ex g being Point of (REAL-NS n) st
for r being Real st 0 < r holds
ex n0 being Nat st
for n1 being Nat st n0 <= n1 holds
||.((s2 . n1) - g).|| < r

take g = g; :: thesis: for r being Real st 0 < r holds
ex n0 being Nat st
for n1 being Nat st n0 <= n1 holds
||.((s2 . n1) - g).|| < r

hereby :: thesis: verum

let r be Real; :: thesis: ( 0 < r implies ex n0 being Nat st
for n1 being Nat st n0 <= n1 holds
||.((s2 . n1) - g).|| < r )
assume 0 < r ; :: thesis: ex n0 being Nat st
for n1 being Nat st n0 <= n1 holds
||.((s2 . n1) - g).|| < r
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: verum

take n0 = n0; :: thesis: for n1 being Nat st n0 <= n1 holds
||.((s2 . n1) - g).|| < r

hereby :: thesis: verum

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

end;

end;

end;

end;

hence s2 is convergent ; :: thesis: verum

end;

assume s2 is convergent ; :: thesis: s1 is convergent
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: ex x being Element of (Euclid n) st
for r being Real st r > 0 holds
ex m0 being Nat st
for m being Nat st m0 <= m holds
dist ((s1 . m),x) < r

take x = x; :: thesis: for r being Real st r > 0 holds
ex m0 being Nat st
for m being Nat st m0 <= m holds
dist ((s1 . m),x) < r

hereby :: thesis: verum

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

hereby :: thesis: verum

take m0 = m0; :: thesis: for m being Nat st m0 <= m holds
dist ((s1 . m),x) < r

hereby :: thesis: verum

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

end;

end;

end;

end;

hence s1 is convergent ; :: thesis: verum