theorem Th52: :: MATRIX11:52

for n being Nat
for K being commutative Ring
for a being Element of K
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,(a * (Line (A,j))))) = 0. K