theorem :: MATRIX_3:8

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