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 A1: 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;
A2: Mx2Tran M is one-to-one by A1, 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 A3: 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 A2, CARD_1:33;
then A4: 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 A5: v in Affin Affn ; :: thesis: v |-- EN = ((Mx2Tran M) . v) |-- ME
set MTv = (Mx2Tran M) . v;
A6: len (v |-- EN) = card Affn by Th16;
A7: len (((Mx2Tran M) . v) |-- ME) = card ((Mx2Tran M) .: Affn) by Th16;

now :: thesis: for i being Nat st 1 <= i & i <= card Affn holds
(v |-- EN) . i = (((Mx2Tran M) . v) |-- ME) . i

let i be Nat; :: thesis: ( 1 <= i & i <= card Affn implies (v |-- EN) . i = (((Mx2Tran M) . v) |-- ME) . i )
assume A8: ( 1 <= i & i <= card Affn ) ; :: thesis: (v |-- EN) . i = (((Mx2Tran M) . v) |-- ME) . i
then A9: i in dom (((Mx2Tran M) . v) |-- ME) by A4, A7, FINSEQ_3:25;
then A10: i in dom ME by FUNCT_1:11;
A11: i in dom (v |-- EN) by A6, A8, 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 A11, FUNCT_1:12
.= (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: Affn)) . ((Mx2Tran M) . Ei) by A1, A5, MATRTOP2:25
.= (((Mx2Tran M) . v) |-- ((Mx2Tran M) .: Affn)) . (ME . i) by A3, A10, FUNCT_1:12
.= (((Mx2Tran M) . v) |-- ME) . i by A9, FUNCT_1:12 ; :: thesis: verum

end;

hence v |-- EN = ((Mx2Tran M) . v) |-- ME by A4, A7, A6; :: thesis: verum