:: deftheorem Def4 defines -convergent NDIFF_1:def 4 :
for S being RealNormSpace
for x being Point of S
for IT being sequence of S holds
( IT is x -convergent iff ( IT is convergent & lim IT = x ) );