let n be Nat; :: thesis: 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 )
let F be one-to-one FinSequence of (TOP-REAL 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 f = F as FinSequence of (n -VectSp_over F_Real) by Lm1;
set M = FinS2MX f;
lines (FinS2MX f) is linearly-independent by A1, Th7;
then A2: the_rank_of (FinS2MX f) = len F by MATRIX13:121;
then consider A being Matrix of n -' (len F),n,F_Real such that
A3: the_rank_of ((FinS2MX f) ^ A) = n by MATRTOP1:16;
len F <= width (FinS2MX f) by A2, MATRIX13:74;
then len F <= n by MATRIX_0:23;
then n - (len F) = n -' (len F) by XREAL_1:233;
then reconsider MA = (FinS2MX f) ^ A as Matrix of n,F_Real ;
take MA ; :: thesis: ( MA is invertible & MA | (len F) = F )
Det MA <> 0. F_Real by A3, MATRIX13:83;
hence MA is invertible by LAPLACE:34; :: thesis: MA | (len F) = F
thus F = MA | (dom F) by FINSEQ_1:21
.= MA | (len F) by FINSEQ_1:def 3 ; :: thesis: verum