let m be Nat; 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; 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; 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; ( 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 RELAT_1:70;
hence
rng (b1 | m) is linearly-independent Subset of V1
by A1, VECTSP_7:1, XBOOLE_1:1; 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; ( A = rng (b1 | m) implies b1 | m is OrdBasis of Lin A )
assume A2:
A = rng (b1 | m)
; b1 | m is OrdBasis of Lin A
A3:
A c= the carrier of (Lin A)
A is linearly-independent
by A1, A2, RELAT_1:70, VECTSP_7:1;
then reconsider A9 = A as linearly-independent Subset of (Lin A) by A3, VECTSP_9:12;
b1 is one-to-one
by MATRLIN:def 2;
then A4:
b1 | m is one-to-one
by FUNCT_1:52;
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; verum