theorem Th92: :: MATRIX13:92

for i, j, m9, n9 being Nat
for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st j in Seg (len M9) & ( i = j implies a <> - (1_ K) ) holds
the_rank_of M9 = the_rank_of (RLine (M9,i,((Line (M9,i)) + (a * (Line (M9,j))))))