theorem :: REAL_NS2:37

for n being Nat
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) )