Basis extension
= 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.