for i being Nat
for K being Field
for a being Element of K
for M being Matrix of K st 1 <= i & i <= width M holds
Col ((a * M),i) = a * (Col (M,i))