theorem :: REAL_NS2:36

for n being 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))