theorem Th3: :: MATRIX12:3

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