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 ) )