theorem Th90: :: MATRIX13:90

for i being Nat
for K being Field
for M being Matrix of K st Line (M,i) = (width M) |-> (0. K) holds
the_rank_of (DelLine (M,i)) = the_rank_of M