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

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