theorem Th69: :: MATRIX15:69

for m, n being Nat
for K being Field
for M being Matrix of n,m,K
for i, j being Nat
for a being Element of K st M is without_repeated_line & j in dom M & ( i = j implies a <> - (1_ K) ) holds
Lin (lines M) = Lin (lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))))