let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real
for A being linearly-independent Subset of (TOP-REAL m) 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 m) st the_rank_of M = n holds
(Mx2Tran M) " A is linearly-independent
let A be linearly-independent Subset of (TOP-REAL m); :: 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 Bm = MX2FinS (1. (F_Real,m)) as OrdBasis of m -VectSp_over F_Real by MATRLIN2:45;
reconsider A1 = A as Subset of (m -VectSp_over F_Real) by Lm1;
reconsider Bn = MX2FinS (1. (F_Real,n)) as OrdBasis of n -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;
A4: Mx2Tran (M1,Bn,Bm) is one-to-one by A1, A3, MATRTOP1:39;
reconsider R = A /\ (rng (Mx2Tran (M1,Bn,Bm))) as Subset of (m -VectSp_over F_Real) ;
A5: R c= A by XBOOLE_1:17;
A1 is linearly-independent by Th7;
then A6: ( dom (Mx2Tran (M1,Bn,Bm)) = [#] (n -VectSp_over F_Real) & R is linearly-independent ) by A5, FUNCT_2:def 1, VECTSP_7:1;
(Mx2Tran (M1,Bn,Bm)) " R is linearly-independent

proof

assume not (Mx2Tran (M1,Bn,Bm)) " R is linearly-independent ; :: thesis: contradiction
then consider L being Linear_Combination of (Mx2Tran (M1,Bn,Bm)) " R such that
A7: Carrier L <> {} and
A8: Sum L = 0. (n -VectSp_over F_Real) by RANKNULL:41;
set C = Carrier L;
A9: Carrier L c= (Mx2Tran (M1,Bn,Bm)) " R by VECTSP_6:def 4;
( (Mx2Tran (M1,Bn,Bm)) .: ((Mx2Tran (M1,Bn,Bm)) " R) = R & (Mx2Tran (M1,Bn,Bm)) @ L is Linear_Combination of (Mx2Tran (M1,Bn,Bm)) .: (Carrier L) ) by FUNCT_1:77, RANKNULL:29, XBOOLE_1:17;
then A10: (Mx2Tran (M1,Bn,Bm)) @ L is Linear_Combination of R by A9, RELAT_1:123, VECTSP_6:4;
(Mx2Tran (M1,Bn,Bm)) | (Carrier L) is one-to-one by A4, FUNCT_1:52;
then A11: Carrier ((Mx2Tran (M1,Bn,Bm)) @ L) = (Mx2Tran (M1,Bn,Bm)) .: (Carrier L) by RANKNULL:39;
(Mx2Tran (M1,Bn,Bm)) | ((Mx2Tran (M1,Bn,Bm)) " R) is one-to-one by A4, FUNCT_1:52;
then Sum ((Mx2Tran (M1,Bn,Bm)) @ L) = (Mx2Tran (M1,Bn,Bm)) . (Sum L) by Th14
.= 0. (m -VectSp_over F_Real) by A8, RANKNULL:9 ;
hence contradiction by A6, A7, A11, A10, VECTSP_7:def 1; :: thesis: verum

end;

then (Mx2Tran (M1,Bn,Bm)) " A is linearly-independent by RELAT_1:133;
hence (Mx2Tran M) " A is linearly-independent by A3, Th7; :: thesis: verum