:: deftheorem Def14 defines * CLVECT_1:def 14 :
for CNS being ComplexLinearSpace
for S being sequence of CNS
for z being Complex
for b₄ being sequence of CNS holds
( b₄ = z * S iff for n being Nat holds b₄ . n = z * (S . n) );