theorem :: MATRLIN2:49

for K being Field
for V1, V2 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for b2 being OrdBasis of V2
for M being Matrix of len b1, len b2,K holds rank (Mx2Tran (M,b1,b2)) = the_rank_of M