theorem :: MATRIX_3:10

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 = 0. K