:: deftheorem defines convergent TOPRNS_1:def 8 :
for N being Nat
for IT being Real_Sequence of N holds
( IT is convergent iff ex g being Point of (TOP-REAL N) st
for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
|.((IT . m) - g).| < r );