theorem :: MATRIX_3:9

for n being Nat
for K being Ring
for l, j being Nat st [l,j] in Indices (1. (K,n)) & l = j holds
(Col ((1. (K,n)),j)) . l = 1. K