for m being Nat
for K being Field
for A, B being Matrix of K st B = 0. (K,(len A),m) holds
the_rank_of A = the_rank_of (A ^^ B)