theorem Th16: :: MATRIX_3:16

for n being Nat
for K being Ring
for i, j being Nat st [i,j] in Indices (1. (K,n)) holds
( ( i = j implies (Col ((1. (K,n)),j)) . i = 1. K ) & ( i <> j implies (Col ((1. (K,n)),j)) . i = 0. K ) )