let n be Nat; :: thesis: for A, B being linearly-independent Subset of (REAL-NS n) st card A = card B holds
ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )
let A, B be linearly-independent Subset of (REAL-NS n); :: thesis: ( card A = card B implies ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) ) )
assume A1: card A = card B ; :: thesis: ex M being Matrix of n,F_Real st
( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )
reconsider A0 = A, B0 = B as Subset of (TOP-REAL n) by Th4;
( A0 is linearly-independent Subset of (TOP-REAL n) & B0 is linearly-independent Subset of (TOP-REAL n) ) by Th28;
then consider M being Matrix of n,F_Real such that
A2: ( M is invertible & (Mx2Tran M) .: ([#] (Lin A0)) = [#] (Lin B0) ) by A1, MATRTOP2:22;
take M ; :: thesis: ( M is invertible & (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) )
thus M is invertible by A2; :: thesis: (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B)
( [#] (Lin A0) = [#] (Lin A) & [#] (Lin B0) = [#] (Lin B) ) by Th26;
hence (Mx2Tran M) .: ([#] (Lin A)) = [#] (Lin B) by A2; :: thesis: verum