theorem :: MATRTOP1:17

for n, m being Nat
for K being Field
for A being Matrix of n,m,K st the_rank_of A = m holds
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n