theorem Th15: :: MATRIX_3:15

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 (Line ((1. (K,n)),i)) . j = 1. K ) & ( i <> j implies (Line ((1. (K,n)),i)) . j = 0. K ) )