theorem :: MATRIX12:21

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