theorem :: MATRLIN2:22

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