theorem Th117: :: MATRIX13:117

for m, n being Nat
for K being Field
for a being Element of K
for M being Matrix of m,n,K st lines M is linearly-independent & M is without_repeated_line holds
for i, j being Nat st j in Seg (len M) & i <> j holds
( RLine (M,i,((Line (M,i)) + (a * (Line (M,j))))) is without_repeated_line & lines (RLine (M,i,((Line (M,i)) + (a * (Line (M,j)))))) is linearly-independent )