theorem Th3: :: MATRIX12:3

for n, m being Nat
for K being non empty multMagma
for a being Element of K
for M being Matrix of n,m,K
for i, j being Nat st i in dom M & j in Seg (width M) holds
(a * (Line (M,i))) . j = a * (M * (i,j))