:: deftheorem defines convergent BHSP_2:def 1 :
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is convergent iff ex g being Point of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),g) < r );