Basis extension

Every linearly independent subset of a finite-dimensional vector space extends to a basis. Starting with its vectors, add a vector outside their current span until the span is the whole space. Each addition preserves linear independence, and the process stops because the dimension is finite. This also lets a linear functional on a vector subspace extend to the ambient space by assigning arbitrary values on the additional basis vectors.