theorem :: MATRIX_3:7

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