> [!NOTE] Theorem
> Let $V$ be a [[Finite Dimensional Real Vector Space|finite dimensional real vector space]]. The any two [[Basis of a Real Vector Space|bases]] of $V$ are [[Finite Set|finite]] and have the same [[Cardinality|cardinality]].
**Proof**: Since $V$ is finite dimensional, by [[Existence of Basis of Finite Dimensional Real Vector Space contains Basis (Sifting Lemma)|sifting lemma]], it has a finite basis. Let $B=\{ v_{1},\dots,v_{n} \}$ be the smallest basis of $V$.
Let $B' \subset V$ be any other basis with $\geq n$ elements. Pick any $w_{1}\in B'$. By [[Replacing a Basis Element with a Nonzero Linear Combination Forms a New Basis of Finite Dimensional Real Vector Space (Exchange Lemma)|exchange Lemma]], there is some $v_{j}\in B$ that we may remove and replace by $w_{1}$ so that $B_{1} = \{ w_{1},\dots,v_{n} \}$is a basis of $V$.
Next pick any element $w_{2}\in B_{1} \setminus \{ w_{1} \}$. Then there exists scalars such that $\lambda_{1}\dots\lambda_{n}$ s.t. $w_{2}=\lambda_{1}w_{1}+\dots+\lambda_{n}w_{n}$but $w_{1},w_{2}$ are linearly independent so $w_{2}=\lambda_{1}w_{1}$ is impossible. Therefore, by exchange lemma, there is some $v_{j}\in B_{1}$ such that $B_{2} = \{ w_{1}, w_{2}, v_{3},\dots, v_{n} \}$is a basis of $V$.
Proceeding inductively, we reach the point where we have constructed a basis $B_{n}= \{ w_{1},\dots,w_{n} \}.$Now if $B'$ has
gt;n$ elements, we can continue to pick an element $w_{n+1}\in B' \setminus B_{n}$. Since $B_{n}$ is a basis, there are scalars $\mu_{i}\in\mathbb{R}$ so that $w_{n+1}=\mu_{1}w_{1}+\dots+w_{n}$which gives a nontrivial dependence linear dependence relation among some elements of $B'$ which contradicts the fact that $B'$ is linearly independent.
Deduce that $\#B' = n = \#B$ as claimed. $\square$