theorem :: REAL_NS2:35

for n being Nat
for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds
ex M being Matrix of n,REAL st
( M is invertible & M | (len F) = F )