theorem Th75: :: MATRIX15:75

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