let n, m be Nat; :: thesis: for Affn being affinely-independent Subset of (TOP-REAL n)
for EN being Enumeration of Affn
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
let Affn be affinely-independent Subset of (TOP-REAL n); :: thesis: for EN being Enumeration of Affn
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
let EN be Enumeration of Affn; :: thesis: for M being Matrix of n,m,F_Real st the_rank_of M = n holds
for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
set TRn = TOP-REAL n;
let M be Matrix of n,m,F_Real; :: thesis: ( the_rank_of M = n implies for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME )
assume A2: the_rank_of M = n ; :: thesis: for ME being Enumeration of (Mx2Tran M) .: Affn st ME = (Mx2Tran M) * EN holds
for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
set MT = Mx2Tran M;
A3: Mx2Tran M is one-to-one by A2, MATRTOP1:39;
set E = EN;
set A = Affn;
let ME be Enumeration of (Mx2Tran M) .: Affn; :: thesis: ( ME = (Mx2Tran M) * EN implies for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME )
assume A4: ME = (Mx2Tran M) * EN ; :: thesis: for pn being Point of (TOP-REAL n) st pn in Affin Affn holds
pn |-- EN = ((Mx2Tran M) . pn) |-- ME
dom (Mx2Tran M) = the carrier of (TOP-REAL n) by FUNCT_2:def 1;
then Affn,(Mx2Tran M) .: Affn are_equipotent by A3, CARD_1:33;
then A5: card Affn = card ((Mx2Tran M) .: Affn) by CARD_1:5;
let v be Element of (TOP-REAL n); :: thesis: ( v in Affin Affn implies v |-- EN = ((Mx2Tran M) . v) |-- ME )
assume A6: v in Affin Affn ; :: thesis: v |-- EN = ((Mx2Tran M) . v) |-- ME
set MTv = (Mx2Tran M) . v;
A7: len (v |-- EN) = card Affn by Th16;
A8: len (((Mx2Tran M) . v) |-- ME) = card ((Mx2Tran M) .: Affn) by Th16;

now

let i be Nat; :: thesis: ( 1 <= i & i <= card Affn implies (v |-- EN) . i = (((Mx2Tran M) . v) |-- ME) . i )
assume A9: ( 1 <= i & i <= card Affn ) ; :: thesis: (v |-- EN) . i = (((Mx2Tran M) . v) |-- ME) . i
then A10: i in dom (((Mx2Tran M) . v) |-- ME) by A5, A8, FINSEQ_3:25;
then A11: i in dom ME by FUNCT_1:11;
A12: i in dom (v |-- EN) by A7, A9, FINSEQ_3:25;
then i in dom EN by FUNCT_1:11;
then EN . i in rng EN by FUNCT_1:def 3;
then reconsider Ei = EN . i as Element of (TOP-REAL n) ;
thus (v |-- EN) . i = (v |-- Affn) . Ei by A12, FUNCT_1:12
.= (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: Affn)) . ((Mx2Tran M) . Ei) by A2, A6, MATRTOP2:25
.= (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: Affn)) . (ME . i) by A4, A11, FUNCT_1:12
.= (((Mx2Tran M) . v) |-- ME) . i by A10, FUNCT_1:12 ; :: thesis: verum

end;

hence v |-- EN = ((Mx2Tran M) . v) |-- ME by A5, A8, A7, FINSEQ_1:14; :: thesis: verum