theorem :: MATRIX12:18

for k, l, n being Nat
for K being comRing
for A being Matrix of n,K st l in dom (1. (K,n)) & k in dom (1. (K,n)) & n > 0 holds
A * (ICol ((1. (K,n)),l,k)) = ICol (A,l,k)