let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is linearly-independent
let M be Matrix of n,m,F_Real; :: thesis: for A being linearly-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is linearly-independent
let A be linearly-independent Subset of (TOP-REAL n); :: thesis: ( the_rank_of M = n implies (Mx2Tran M) .: A is linearly-independent )
assume A1: the_rank_of M = n ; :: thesis: (Mx2Tran M) .: A is linearly-independent
set nV = n -VectSp_over F_Real;
set mV = 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 MATRTOP1:19;
len Bn = n by MATRTOP1:19;
then reconsider M1 = M as Matrix of len Bn, len Bm,F_Real by A2;
set MT = Mx2Tran (M1,Bn,Bm);
A3: Mx2Tran M = Mx2Tran (M1,Bn,Bm) by MATRTOP1:20;
reconsider A1 = A as Subset of (n -VectSp_over F_Real) by Lm1;
A4: A1 is linearly-independent by Th7;
(Mx2Tran (M1,Bn,Bm)) .: A1 is linearly-independent

proof

assume not (Mx2Tran (M1,Bn,Bm)) .: A1 is linearly-independent ; :: thesis: contradiction
then consider L being Linear_Combination of (Mx2Tran (M1,Bn,Bm)) .: A1 such that
A5: Carrier L <> {} and
A6: Sum L = 0. (m -VectSp_over F_Real) by RANKNULL:41;
A7: Mx2Tran (M1,Bn,Bm) is one-to-one by A1, A3, MATRTOP1:39;
then A8: ker (Mx2Tran (M1,Bn,Bm)) = (0). (n -VectSp_over F_Real) by RANKNULL:15;
A9: (Mx2Tran (M1,Bn,Bm)) | A1 is one-to-one by A7, FUNCT_1:52;
then A10: (Mx2Tran (M1,Bn,Bm)) @ ((Mx2Tran (M1,Bn,Bm)) # L) = L by RANKNULL:43;
(Mx2Tran (M1,Bn,Bm)) | (Carrier ((Mx2Tran (M1,Bn,Bm)) # L)) is one-to-one by A7, FUNCT_1:52;
then (Mx2Tran (M1,Bn,Bm)) .: (Carrier ((Mx2Tran (M1,Bn,Bm)) # L)) = Carrier L by A10, RANKNULL:39;
then A11: Carrier ((Mx2Tran (M1,Bn,Bm)) # L) <> {} by A5;
(Mx2Tran (M1,Bn,Bm)) . (Sum ((Mx2Tran (M1,Bn,Bm)) # L)) = 0. (m -VectSp_over F_Real) by A6, A9, A10, Th14;
then Sum ((Mx2Tran (M1,Bn,Bm)) # L) in ker (Mx2Tran (M1,Bn,Bm)) by RANKNULL:10;
then Sum ((Mx2Tran (M1,Bn,Bm)) # L) = 0. (n -VectSp_over F_Real) by A8, VECTSP_4:35;
hence contradiction by A4, A11, VECTSP_7:def 1; :: thesis: verum

end;

hence (Mx2Tran M) .: A is linearly-independent by A3, Th7; :: thesis: verum