theorem Th93: :: MATRIX13:93

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) & j <> i holds
the_rank_of (DelLine (M9,i)) = the_rank_of (RLine (M9,i,(a * (Line (M9,j)))))