for n being Nat
for K being commutative Ring
for A being Matrix of n,K st not K is degenerated & K is well-unital & K is domRing-like holds
for i, j being Nat st i in Seg n & j in Seg n & i <> j holds
Det (RLine (A,i,(Line (A,j)))) = 0. K