:: deftheorem Def6 defines * MATRIXC1:def 6 :
for M being Matrix of COMPLEX
for F, b₃ being FinSequence of COMPLEX holds
( b₃ = M * F iff ( len b₃ = len M & ( for i being Nat st i in Seg (len M) holds
b₃ . i = Sum (mlt ((Line (M,i)),F)) ) ) );