theorem :: MATRIX15:76

for n being Nat
for K being Field
for A being Matrix of n,n,K
for B being Matrix of K st len A = width B & Det A <> 0. K holds
the_rank_of (B * A) = the_rank_of B