let m be Nat; :: thesis: for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds
( rng (b1 /^ m) is linearly-independent Subset of V1 & ( for A being Subset of V1 st A = rng (b1 /^ m) holds
b1 /^ m is OrdBasis of Lin A ) )
let K be Field; :: thesis: for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1 holds
( rng (b1 /^ m) is linearly-independent Subset of V1 & ( for A being Subset of V1 st A = rng (b1 /^ m) holds
b1 /^ m is OrdBasis of Lin A ) )
let V1 be finite-dimensional VectSp of K; :: thesis: for b1 being OrdBasis of V1 holds
( rng (b1 /^ m) is linearly-independent Subset of V1 & ( for A being Subset of V1 st A = rng (b1 /^ m) holds
b1 /^ m is OrdBasis of Lin A ) )
let b1 be OrdBasis of V1; :: thesis: ( rng (b1 /^ m) is linearly-independent Subset of V1 & ( for A being Subset of V1 st A = rng (b1 /^ m) holds
b1 /^ m is OrdBasis of Lin A ) )
reconsider RNG = rng b1 as Basis of V1 by MATRLIN:def 2;
A1: RNG is linearly-independent by VECTSP_7:def 3;
rng (b1 /^ m) c= RNG by FINSEQ_5:33;
hence rng (b1 /^ m) is linearly-independent Subset of V1 by A1, VECTSP_7:1, XBOOLE_1:1; :: thesis: for A being Subset of V1 st A = rng (b1 /^ m) holds
b1 /^ m is OrdBasis of Lin A
let A be Subset of V1; :: thesis: ( A = rng (b1 /^ m) implies b1 /^ m is OrdBasis of Lin A )
assume A2: A = rng (b1 /^ m) ; :: thesis: b1 /^ m is OrdBasis of Lin A
A3: A c= the carrier of (Lin A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the carrier of (Lin A) )
assume x in A ; :: thesis: x in the carrier of (Lin A)
then x in Lin A by VECTSP_7:8;
hence x in the carrier of (Lin A) ; :: thesis: verum

end;

A is linearly-independent by A1, A2, FINSEQ_5:33, VECTSP_7:1;
then reconsider A9 = A as linearly-independent Subset of (Lin A) by A3, VECTSP_9:12;
( b1 is one-to-one & b1 = (b1 | m) ^ (b1 /^ m) ) by MATRLIN:def 2, RFINSEQ:8;
then A4: b1 /^ m is one-to-one by FINSEQ_3:91;
Lin A9 = ModuleStr(# the carrier of (Lin A), the addF of (Lin A), the ZeroF of (Lin A), the lmult of (Lin A) #) by VECTSP_9:17;
then ( rng (b1 /^ m) is Basis of (Lin A) & b1 /^ m is FinSequence of (Lin A) ) by A2, FINSEQ_1:def 4, VECTSP_7:def 3;
hence b1 /^ m is OrdBasis of Lin A by A4, MATRLIN:def 2; :: thesis: verum