let n be Nat; :: thesis: for F being one-to-one FinSequence of (REAL-NS n) st rng F is linearly-independent holds
for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
let F be one-to-one FinSequence of (REAL-NS n); :: thesis: ( rng F is linearly-independent implies for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) )
assume A1: rng F is linearly-independent ; :: thesis: for B being OrdBasis of n -VectSp_over F_Real st B = MX2FinS (1. (F_Real,n)) holds
for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
let B be OrdBasis of n -VectSp_over F_Real; :: thesis: ( B = MX2FinS (1. (F_Real,n)) implies for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) )
assume A2: B = MX2FinS (1. (F_Real,n)) ; :: thesis: for M being Matrix of n,F_Real st M is invertible & M | (len F) = F holds
(Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
let M be Matrix of n,F_Real; :: thesis: ( M is invertible & M | (len F) = F implies (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) )
assume A3: ( M is invertible & M | (len F) = F ) ; :: thesis: (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F))
reconsider F0 = F as FinSequence of (TOP-REAL n) by Th4;
rng F0 is linearly-independent by A1, Th28;
then (Mx2Tran M) .: ([#] (Lin (rng (B | (len F0))))) = [#] (Lin (rng F0)) by A2, A3, MATRTOP2:21;
hence (Mx2Tran M) .: ([#] (Lin (rng (B | (len F))))) = [#] (Lin (rng F)) by Th26; :: thesis: verum