let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real
for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is affinely-independent
let M be Matrix of n,m,F_Real; :: thesis: for A being affinely-independent Subset of (TOP-REAL n) st the_rank_of M = n holds
(Mx2Tran M) .: A is affinely-independent
set MT = Mx2Tran M;
set TRn = TOP-REAL n;
set TRm = TOP-REAL m;
let A be affinely-independent Subset of (TOP-REAL n); :: thesis: ( the_rank_of M = n implies (Mx2Tran M) .: A is affinely-independent )
assume A1: the_rank_of M = n ; :: thesis: (Mx2Tran M) .: A is affinely-independent

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: (Mx2Tran M) .: A is affinely-independent

then (Mx2Tran M) .: A is empty ;
hence (Mx2Tran M) .: A is affinely-independent ; :: thesis: verum

end;

suppose not A is empty ; :: thesis: (Mx2Tran M) .: A is affinely-independent

then consider v being Element of (TOP-REAL n) such that
A2: v in A and
A3: ((- v) + A) \ {(0. (TOP-REAL n))} is linearly-independent by RLAFFIN1:def 4;
A4: dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def 1;
then A5: (Mx2Tran M) . v in (Mx2Tran M) .: A by A2, FUNCT_1:def 6;
(Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m) by MATRTOP1:29;
then A6: {(0. (TOP-REAL m))} = Im ((Mx2Tran M),(0. (TOP-REAL n))) by A4, FUNCT_1:59
.= (Mx2Tran M) .: {(0. (TOP-REAL n))} by RELAT_1:def 16 ;
- v = (0. (TOP-REAL n)) - v by RLVECT_1:14;
then A7: (Mx2Tran M) . (- v) = ((Mx2Tran M) . (0. (TOP-REAL n))) - ((Mx2Tran M) . v) by MATRTOP1:28
.= (0. (TOP-REAL m)) - ((Mx2Tran M) . v) by MATRTOP1:29
.= - ((Mx2Tran M) . v) by RLVECT_1:14 ;
Mx2Tran M is one-to-one by A1, MATRTOP1:39;
then A8: (Mx2Tran M) .: (((- v) + A) \ {(0. (TOP-REAL n))}) = ((Mx2Tran M) .: ((- v) + A)) \ ((Mx2Tran M) .: {(0. (TOP-REAL n))}) by FUNCT_1:64
.= ((- ((Mx2Tran M) . v)) + ((Mx2Tran M) .: A)) \ {(0. (TOP-REAL m))} by A6, A7, MATRTOP1:30 ;
(Mx2Tran M) .: (((- v) + A) \ {(0. (TOP-REAL n))}) is linearly-independent by A1, A3, Th23;
hence (Mx2Tran M) .: A is affinely-independent by A5, A8, RLAFFIN1:def 4; :: thesis: verum

end;

end;