let n be Nat; :: thesis: for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds
ex M being Matrix of n,F_Real st
( M is invertible & M | (len F) = F )
let F be one-to-one FinSequence of (REAL-NS n); :: thesis: ( rng F is linearly-independent implies ex M being Matrix of n,F_Real st
( M is invertible & M | (len F) = F ) )
assume A1: rng F is linearly-independent ; :: thesis: ex M being Matrix of n,F_Real st
( M is invertible & M | (len F) = F )
reconsider F0 = F as FinSequence of (TOP-REAL n) by Th4;
rng F0 is linearly-independent by A1, Th28;
then consider M being Matrix of n,F_Real such that
A2: ( M is invertible & M | (len F0) = F0 ) by MATRTOP2:19;
take M ; :: thesis: ( M is invertible & M | (len F) = F )
thus ( M is invertible & M | (len F) = F ) by A2; :: thesis: verum