for m, n being Nat
for V1 being free finite-rank Z_Module
for M being Matrix of n,m,INT.Ring st n > 0 & m > 0 holds
for p, d being FinSequence of INT.Ring 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))