Let V be a vector space and v1,…,vm, w1,…,wn ∈ V. If the vi are linearly independent and the wi span V, then, with some possible reordering of the wi,
spans V. Thus, each vi can be introduced one at a time in exchange for some wj and consequentially m ≤ n. This implies all bases of V have the same cardinality and that the dimension of V is well defined.