for m, n being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for M being Matrix of n,m, the carrier of K st n > 0 & m > 0 holds
for p, d being FinSequence of K st len p = n & len d = m & ( for j being Nat st j in dom d holds
d /. j = Sum (mlt (p,(Col (M,j)))) ) holds
for b, c being FinSequence of V1 st len b = m & len c = n & ( for i being Nat st i in dom c holds
c /. i = Sum (lmlt ((Line (M,i)),b)) ) holds
Sum (lmlt (p,c)) = Sum (lmlt (d,b))