let n, m be Nat; :: thesis: for Affn being affinely-independent Subset of ()
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 () .: Affn st ME = () * EN holds
for pn being Point of () st pn in Affin Affn holds
pn |-- EN = (() . pn) |-- ME

let Affn be affinely-independent Subset of (); :: 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 () .: Affn st ME = () * EN holds
for pn being Point of () st pn in Affin Affn holds
pn |-- EN = (() . 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 () .: Affn st ME = () * EN holds
for pn being Point of () st pn in Affin Affn holds
pn |-- EN = (() . 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 () .: Affn st ME = () * EN holds
for pn being Point of () st pn in Affin Affn holds
pn |-- EN = (() . pn) |-- ME )

assume A1: the_rank_of M = n ; :: thesis: for ME being Enumeration of () .: Affn st ME = () * EN holds
for pn being Point of () st pn in Affin Affn holds
pn |-- EN = (() . pn) |-- ME

set MT = Mx2Tran M;
A2: Mx2Tran M is one-to-one by ;
set E = EN;
set A = Affn;
let ME be Enumeration of () .: Affn; :: thesis: ( ME = () * EN implies for pn being Point of () st pn in Affin Affn holds
pn |-- EN = (() . pn) |-- ME )

assume A3: ME = () * EN ; :: thesis: for pn being Point of () st pn in Affin Affn holds
pn |-- EN = (() . pn) |-- ME

dom () = the carrier of () by FUNCT_2:def 1;
then Affn,(Mx2Tran M) .: Affn are_equipotent by ;
then A4: card Affn = card (() .: Affn) by CARD_1:5;
let v be Element of (); :: thesis: ( v in Affin Affn implies v |-- EN = (() . v) |-- ME )
assume A5: v in Affin Affn ; :: thesis: v |-- EN = (() . v) |-- ME
set MTv = () . v;
A6: len (v |-- EN) = card Affn by Th16;
A7: len ((() . v) |-- ME) = card (() .: Affn) by Th16;
now :: thesis: for i being Nat st 1 <= i & i <= card Affn holds
(v |-- EN) . i = ((() . v) |-- ME) . i
let i be Nat; :: thesis: ( 1 <= i & i <= card Affn implies (v |-- EN) . i = ((() . v) |-- ME) . i )
assume A8: ( 1 <= i & i <= card Affn ) ; :: thesis: (v |-- EN) . i = ((() . v) |-- ME) . i
then A9: i in dom ((() . v) |-- ME) by ;
then A10: i in dom ME by FUNCT_1:11;
A11: i in dom (v |-- EN) by ;
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 () ;
thus (v |-- EN) . i = (v |-- Affn) . Ei by
.= ((() . v) |-- (() .: Affn)) . (() . Ei) by
.= ((() . v) |-- (() .: Affn)) . (ME . i) by
.= ((() . v) |-- ME) . i by ; :: thesis: verum
end;
hence v |-- EN = (() . v) |-- ME by A4, A7, A6; :: thesis: verum