:: deftheorem Def3 defines bounded BHSP_3:def 3 :
for X being RealUnitarySpace
for seq being sequence of X holds
( seq is bounded iff ex M being Real st
( M > 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) ) );