theorem :: MATRIXR1:20

for K being non empty multMagma
for a being Element of K
for M being Matrix of K
for i being Nat st 1 <= i & i <= len M holds
Line ((a * M),i) = a * (Line (M,i))