Choice-free Hahn-Banach extension in a separable space ($\tilde{T}{|}_U=T,\Vert \tilde{T}\Vert =\Vert T\Vert$)

In a real normed vector space with a specified countable dense subset, a bounded linear functional on any vector subspace admits a norm-preserving extension without the axiom of choice. Add the dense vectors one at a time using the supremum endpoint in the one-dimensional dominated extension of a real linear functional. This makes the recursion deterministic. Extend from the resulting dense subspace by continuity, using the least index in the dense list which approximates a given vector to within $2^{-n}$.