let n be Nat; 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); ( 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
; 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; ( 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))
; 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; ( 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 )
; (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; verum