for K being Field
for A, B being Matrix of K st len A = len B holds
( the_rank_of A <= the_rank_of (A ^^ B) & the_rank_of B <= the_rank_of (A ^^ B) )