:: deftheorem Def3 defines ||. BHSP_2:def 3 :
for X being RealUnitarySpace
for seq being sequence of X
for b₃ being Real_Sequence holds
( b₃ = ||.seq.|| iff for n being Nat holds b₃ . n = ||.(seq . n).|| );