:: deftheorem Def9 defines mlt MATRIXJ1:def 9 :
for K being Field
for G being FinSequence_of_Matrix of K
for p being FinSequence of K
for b₄ being FinSequence_of_Matrix of K holds
( b₄ = mlt (p,G) iff ( dom b₄ = dom G & ( for i being Nat st i in dom b₄ holds
b₄ . i = (p /. i) * (G . i) ) ) );