for i, m9, n9 being Nat
for K being Field
for a being Element of K
for M9 being Matrix of n9,m9,K st a <> 0. K holds
the_rank_of M9 = the_rank_of (RLine (M9,i,(a * (Line (M9,i)))))