:: deftheorem Def1 defines Cauchy BHSP_3:def 1 :
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r );