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,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,REAL st
( M is invertible & M | (len F) = F ) )
assume rng F is linearly-independent ; :: thesis: ex M being Matrix of n,REAL st
( M is invertible & M | (len F) = F )
then consider M being Matrix of n,F_Real such that
A1: ( M is invertible & M | (len F) = F ) by Th32;
reconsider N = MXF2MXR M as Matrix of n,REAL ;
take N ; :: thesis: ( N is invertible & N | (len F) = F )
thus N is invertible by A1, Th33; :: thesis: N | (len F) = F
thus N | (len F) = F by A1; :: thesis: verum