[proofplan]
The double annihilator first lives in $V^{**}$, so we compare it with $U$ through the evaluation isomorphism $V \cong V^{**}$. We prove the inclusion $\operatorname{ev}(U) \subset (U^0)^0$ directly from the definition of $U^0$. Then we compute dimensions using the finite-dimensional annihilator dimension formula, first for $U \subset V$ and then for $U^0 \subset V^*$. The inclusion and equal dimensions force equality.
[/proofplan]
[step:Identify $V$ with $V^{**}$ through evaluation]
Define the evaluation map
\begin{align*}
\operatorname{ev}: V &\to V^{**}
\end{align*}
by the rule
\begin{align*}
\operatorname{ev}(v)(\lambda)=\lambda(v)
\end{align*}
for every $v \in V$ and every $\lambda \in V^*$. Since $V$ is finite-dimensional over $k$, this map is a $k$-linear isomorphism. We will regard $(U^0)^0 \subset V^{**}$ as a subspace of $V$ via this isomorphism; equivalently, it is enough to prove
\begin{align*}
(U^0)^0=\operatorname{ev}(U)
\end{align*}
inside $V^{**}$.
[/step]
[step:Show every vector in $U$ annihilates every functional in $U^0$]
Let $u \in U$. To prove $\operatorname{ev}(u) \in (U^0)^0$, let $\lambda \in U^0$. By the definition of $U^0$, the functional $\lambda$ vanishes on every element of $U$, so in particular
\begin{align*}
\lambda(u)=0.
\end{align*}
Therefore
\begin{align*}
\operatorname{ev}(u)(\lambda)=\lambda(u)=0.
\end{align*}
Since this holds for every $\lambda \in U^0$, we have $\operatorname{ev}(u) \in (U^0)^0$. Hence
\begin{align*}
\operatorname{ev}(U) \subset (U^0)^0.
\end{align*}
[guided]
The first goal is to prove containment, not equality. Equality is easier after we know the dimensions agree, so we begin by checking that every element of $U$ gives an element of the double annihilator.
Take an arbitrary vector $u \in U$. Under the evaluation map, this vector corresponds to the functional
\begin{align*}
\operatorname{ev}(u): V^* &\to k
\end{align*}
defined by
\begin{align*}
\operatorname{ev}(u)(\lambda)=\lambda(u)
\end{align*}
for every $\lambda \in V^*$. To show that $\operatorname{ev}(u)$ lies in $(U^0)^0$, we must verify the defining condition for membership in $(U^0)^0$: it must vanish on every $\lambda \in U^0$.
Let $\lambda \in U^0$. By definition,
\begin{align*}
U^0=\{\mu \in V^* : \mu(x)=0 \text{ for every } x \in U\}.
\end{align*}
Since $u \in U$, this definition gives
\begin{align*}
\lambda(u)=0.
\end{align*}
Therefore
\begin{align*}
\operatorname{ev}(u)(\lambda)=\lambda(u)=0.
\end{align*}
Because the choice of $\lambda \in U^0$ was arbitrary, $\operatorname{ev}(u)$ vanishes on all of $U^0$. Thus $\operatorname{ev}(u) \in (U^0)^0$.
Since the choice of $u \in U$ was arbitrary, every element of $\operatorname{ev}(U)$ lies in $(U^0)^0$, and consequently
\begin{align*}
\operatorname{ev}(U) \subset (U^0)^0.
\end{align*}
[/guided]
[/step]
[step:Compute the dimension of the double annihilator]
By the dimension formula for linear annihilators [citetheorem:7856] applied to the subspace $U \subset V$, we have
\begin{align*}
\dim_k U+\dim_k U^0=\dim_k V.
\end{align*}
Thus
\begin{align*}
\dim_k U^0=\dim_k V-\dim_k U.
\end{align*}
Now apply the same dimension formula to the finite-dimensional vector space $V^*$ and its subspace $U^0 \subset V^*$. The annihilator of $U^0$ in $(V^*)^*=V^{**}$ is precisely $(U^0)^0$, so
\begin{align*}
\dim_k U^0+\dim_k (U^0)^0=\dim_k V^*.
\end{align*}
Since $V$ is finite-dimensional, $\dim_k V^*=\dim_k V$. Therefore
\begin{align*}
\dim_k (U^0)^0=\dim_k V^*-\dim_k U^0.
\end{align*}
Substituting the previous expression for $\dim_k U^0$ gives
\begin{align*}
\dim_k (U^0)^0=\dim_k V-(\dim_k V-\dim_k U)=\dim_k U.
\end{align*}
Because $\operatorname{ev}: V \to V^{**}$ is an isomorphism, we also have
\begin{align*}
\dim_k \operatorname{ev}(U)=\dim_k U.
\end{align*}
[/step]
[step:Conclude equality from inclusion and equal dimension]
We have proved that
\begin{align*}
\operatorname{ev}(U) \subset (U^0)^0.
\end{align*}
Both spaces are finite-dimensional subspaces of $V^{**}$, and the previous step gives
\begin{align*}
\dim_k \operatorname{ev}(U)=\dim_k U=\dim_k (U^0)^0.
\end{align*}
A finite-dimensional subspace contained in another subspace of the same dimension is equal to it. Hence
\begin{align*}
\operatorname{ev}(U)=(U^0)^0.
\end{align*}
Identifying $V$ with $V^{**}$ through $\operatorname{ev}$, this is exactly
\begin{align*}
(U^0)^0=U.
\end{align*}
[/step]
