:: deftheorem Def7 defines * BHSP_4:def 7 :
for X being RealUnitarySpace
for seq being sequence of X
for Rseq being Real_Sequence
for b₄ being sequence of X holds
( b₄ = Rseq * seq iff for n being Nat holds b₄ . n = (Rseq . n) * (seq . n) );