let K be 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
let V1, V2 be 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 b1 be 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 b2 be OrdBasis of V2; 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; 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
; verum