:: deftheorem defines convergent NORMSP_1:def 6 :
for RNS being RealNormSpace
for S being sequence of RNS holds
( S is convergent iff ex g being Point of RNS st
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - g).|| < r );