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