theorem :: MATRIX15:73

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