Inside the space of eventually zero families, the linear subspace spanned by $\{\, e_i : i \ge 1 \,\}$ is proper and has a basis equinumerous with a basis of the whole space, so "equal dimension forces equality" fails without finite dimension

False claim: if $U$ is a linear subspace of a vector space $V$ over $F$ and some basis of $U$ is equinumerous with some basis of $V$, then $U = V$.

Let $F$ be any field, let $E \subseteq F^{\mathbb{N}}$ be the linear subspace of eventually zero families and let $e_k$ be the standard unit families (The standard unit families $e_k \in F^{\mathbb{N}}$ form a basis of the linear subspace of eventually zero families: an explicit infinite basis, built with no choice principle). Put

$B := \{\, e_k : k \in \mathbb{N} \,\}, \qquad B' := \{\, e_k : k \in \mathbb{N},\ k \ge 1 \,\}, \qquad U := \operatorname{span}(B') .$

Then

1. $U$ is a linear subspace of $E$ and $B'$ is a basis of $U$, while $B$ is a basis of $E$;
2. $B' \approx B$ (Equinumerous sets, $A \approx B$ and $A \preceq B$), both being equinumerous with $\mathbb{N}$;
3. $U \ne E$: the family $e_0$ lies in $E$ and not in $U$.

So a proper linear subspace can carry a basis equinumerous with a basis of the whole space, and the equality clause of If $\dim_F V = n$ and $U$ is a linear subspace of $V$, then $U$ is finite-dimensional, $\dim_F U \le n$, and $\dim_F U = n$ if and only if $U = V$ — which is stated only for a finite-dimensional ambient space — really does need its hypothesis.

No dimension is assigned to either space. $E$ and $U$ are both infinite-dimensional (Finite-dimensional vector space, and its dimension $\dim_F V$; infinite-dimensional means having no finite basis assigns no number to such a space): for $E$ this is claim 4 of The standard unit families $e_k \in F^{\mathbb{N}}$ form a basis of the linear subspace of eventually zero families: an explicit infinite basis, built with no choice principle, and for $U$ it follows from claims 1 and 2 below, since the basis $B'$ of $U$ is linearly independent and equinumerous with $\mathbb{N}$, so $U$ can have no finite spanning set and hence no finite basis, by claim 2 of If $V$ has a spanning set with $n$ elements, then every linearly independent subset of $V$ is finite with at most $n$ elements; in particular $V$ has no linearly independent subset equinumerous with $\mathbb{N}$. And claim 2 compares two specific bases through an explicit bijection, not two cardinal numbers.

• The finite case is a theorem, and this shows why it is one. If $\dim_F V = n$ and $U$ is a linear subspace of $V$, then $U$ is finite-dimensional, $\dim_F U \le n$, and $\dim_F U = n$ if and only if $U = V$ proves that in a finite-dimensional ambient space equality of dimensions forces equality of the spaces; its proof enlarges a basis of the subspace by a vector outside it and contradicts the bound on independent sets. Here the same enlargement is possible — $B' \cup \{e_0\} = B$ is independent — and contradicts nothing, because there is no finite bound to violate.

• No cardinal arithmetic is used or implied. The comparison in claim 2 is a named bijection, $k \mapsto e_{\sigma(k)}$, between two specific sets. This item does not assign a dimension to $E$ or to $U$, and it says nothing about whether any two bases of $E$ are equinumerous; that question needs cardinal arithmetic, which is not available at this point in the reading order.

• The subspace is spanned by "all but one" basis vector. Deleting a single element from an infinite basis leaves a set that is still equinumerous with the original, which is exactly the phenomenon The pigeonhole principle on $\mathbb{N}$ rules out for finite sets and for natural numbers.