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