Currently I am reading Simpson's Subsystem of Second Order Arithmetic.
Definition $4.9.2$ The following definitions are made in $RCA_0$: Given a separable Banach space $\hat{A},$ a subspace of $\hat{A}$ consists of a separable Banach space $\hat{S}$ together with a bounded linear operator $\psi:\hat{S}\to\hat{A}$ such that $$\psi(x)\| = \|x\| \quad \text{for all }x\in \hat{S}.$$ We identify $x\in\hat{S}$ with $\psi(x)\in\hat{A}.$ If $\hat{B}$ is another separable Banach space and $F:\hat{S}\to \hat{B}$ is a bounded linear operator, we say that $\tilde{F}:\hat{A}\to\hat{B}$ extends $F$ if $$\tilde{F}(\psi(x)) = F(x) \quad \text{for all }x\in \hat{S}.$$
At Chapter 4 Weak Konig Lemma, section $4.9$ the separable Hahn/Banach Theorem, the author provided a proof for Hahn/Banach Theorem.
Theorem $4.9.13$ The following is provable in $WKL_0.$ Let $\hat{A}$ be a separable Banach space and let $\hat{S}$ be a subspace of $\hat{A}.$ Let $f:\hat{S}\to\mathbb{R}$ be a bounded linear functional such that $\|f\|\leq \alpha,$ where $\alpha$ is a positive real number. Then there exists a bounded linear functional $\tilde{f}:\hat{A}\to\mathbb{R}$ extending $f$ such that $\|\tilde{f}\|\leq\alpha.$
The following is a proof.
Proof: We may safely assume that $\alpha = 1.$ Let $$A = \{a_i:i\in\mathbb{N}\}\quad\text{and}\quad S=\{s_i:\mathbb{N}\}.$$ We may safely assume that $a_0=s_0=0.$ Let $C_0$ be the closed convex set in $\mathbb{R}^n$ consisting of those sequences $\langle z_i:i\in\mathbb{N} \rangle$ such that $z_0=0$ and $$|z_i-z_j|\leq \|a_i-a_j\|$$ for all $I,j\in\mathbb{N}.$ $C_0$ is included in the compact product space $$\prod_{I\in\mathbb{N}}[-\|a_i\|,\|a_i\|].$$ To each $z = \langle z_i:\in\mathbb{N} \rangle \in C_0$ is associated a continuous function $$g=g_z:\hat{A}\to\mathbb{R}$$ such that $g(a_i)=z_i$ for all $I\in\mathbb{N}.$
In the remaining of the proof, the authors defined the following four sets in sequence.
$$C_0= \{ (z_i:i\in\mathbb{N})\in \mathbb{R}^\mathbb{N}: z_0=0, |z_i-z_j|\leq \|a_i-a_j\|, \text{ for all }i,j\in\mathbb{N} \},$$ $$C_1 = \{g\in C_0: g(\psi(s)) = f(s) \text{ for all }s\in \hat{S}\},$$ $$C_2 = \{ g\in C_1: g(x+\psi(s)) = g(x) + g(\psi(s) \text{ for all }x\in \hat{A} \text{ and }s\in \hat{S}) \},$$ $$C_3 = \{g\in C_2: g(x+y) = g(x)+g(y)\}.$$
Question: What is a motivation of defining $C_0?$
I have pondered about it for a few days but not able to solve it.