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 (TOP-REAL n)
for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
let M be Matrix of n,m,F_Real; :: thesis: ( the_rank_of M = n implies for A being finite Subset of (TOP-REAL n)
for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A )
assume A1: the_rank_of M = n ; :: thesis: for A being finite Subset of (TOP-REAL n)
for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
set MT = Mx2Tran M;
A2: Mx2Tran M is one-to-one by A1, MATRTOP1:39;
set TRn = TOP-REAL n;
let A be finite Subset of (TOP-REAL n); :: thesis: for E being Enumeration of A holds (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
let E be Enumeration of A; :: thesis: (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A
A3: rng E = A by Def1;
dom (Mx2Tran M) = [#] (TOP-REAL n) by FUNCT_2:def 1;
then len ((Mx2Tran M) * E) = len E by A3, FINSEQ_2:29;
then A4: dom ((Mx2Tran M) * E) = dom E by FINSEQ_3:29;
rng ((Mx2Tran M) * E) = ((Mx2Tran M) * E) .: (dom ((Mx2Tran M) * E)) by RELAT_1:113
.= (Mx2Tran M) .: (E .: (dom E)) by A4, RELAT_1:126
.= (Mx2Tran M) .: A by A3, RELAT_1:113 ;
hence (Mx2Tran M) * E is Enumeration of (Mx2Tran M) .: A by A2, Def1; :: thesis: verum