let K be Field; :: thesis: 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
let V1, V2 be finite-dimensional VectSp of K; :: thesis: 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
let b1 be OrdBasis of V1; :: thesis: 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
let b2 be OrdBasis of V2; :: thesis: for M being Matrix of len b1, len b2,K holds rank (Mx2Tran M,b1,b2) = the_rank_of M
let M be Matrix of len b1, len b2,K; :: thesis: rank (Mx2Tran M,b1,b2) = the_rank_of M
thus rank (Mx2Tran M,b1,b2) = the_rank_of (AutMt (Mx2Tran M,b1,b2),b1,b2) by Th48
.= the_rank_of M by Th36 ; :: thesis: verum