let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for A being finite Subset of ()
for E being Enumeration of A holds () * E is Enumeration of () .: A

let M be Matrix of n,m,F_Real; :: thesis: ( the_rank_of M = n implies for A being finite Subset of ()
for E being Enumeration of A holds () * E is Enumeration of () .: A )

assume A1: the_rank_of M = n ; :: thesis: for A being finite Subset of ()
for E being Enumeration of A holds () * E is Enumeration of () .: A

set MT = Mx2Tran M;
A2: Mx2Tran M is one-to-one by ;
set TRn = TOP-REAL n;
let A be finite Subset of (); :: thesis: for E being Enumeration of A holds () * E is Enumeration of () .: A
let E be Enumeration of A; :: thesis: () * E is Enumeration of () .: A
A3: rng E = A by Def1;
dom () = [#] () by FUNCT_2:def 1;
then len (() * E) = len E by ;
then A4: dom (() * E) = dom E by FINSEQ_3:29;
rng (() * E) = (() * E) .: (dom (() * E)) by RELAT_1:113
.= () .: (E .: (dom E)) by
.= () .: A by ;
hence (Mx2Tran M) * E is Enumeration of () .: A by ; :: thesis: verum