:: deftheorem Def8 defines * CLVECT_3:def 8 :
for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence
for b₄ being sequence of X holds
( b₄ = Cseq * seq iff for n being Nat holds b₄ . n = (Cseq . n) * (seq . n) );