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 A being Matrix of len b1, len b2,K st the_rank_of A = len b1 holds
Mx2Tran (A,b1,b2) is one-to-one