for n, m being Nat
for M being Matrix of n,m,F_Real
for Bn being OrdBasis of n -VectSp_over F_Real
for Bm being OrdBasis of m -VectSp_over F_Real st Bn = MX2FinS (1. (F_Real,n)) & Bm = MX2FinS (1. (F_Real,m)) holds
for M1 being Matrix of len Bn, len Bm,F_Real st M1 = M holds
Mx2Tran M = Mx2Tran (M1,Bn,Bm)