let n, m be Nat; :: thesis: for M1, M2 being Matrix of n,m,F_Real st Mx2Tran M1 = Mx2Tran M2 holds
M1 = M2
let M1, M2 be Matrix of n,m,F_Real; :: thesis: ( Mx2Tran M1 = Mx2Tran M2 implies M1 = M2 )
assume A1: Mx2Tran M1 = Mx2Tran M2 ; :: thesis: M1 = M2
set Vn = n -VectSp_over F_Real;
set Vm = m -VectSp_over F_Real;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -VectSp_over F_Real by MATRLIN2:45;
reconsider Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
A2: len Bm = m by Th19;
len Bn = n by Th19;
then reconsider A1 = M1, B1 = M2 as Matrix of len Bn, len Bm,F_Real by A2;
A3: Mx2Tran (A1,Bn,Bm) = Mx2Tran M1 by Th20
.= Mx2Tran (B1,Bn,Bm) by A1, Th20 ;
thus M1 = AutMt ((Mx2Tran (A1,Bn,Bm)),Bn,Bm) by MATRLIN2:36
.= M2 by A3, MATRLIN2:36 ; :: thesis: verum