The development is dual to the Kolmogorov one (Theorem 3.8) under the domain \(\leftrightarrow \) codomain swap: where the Kolmogorov numbers push \(S\) down a quotient projection \(\pi _V : Y \to Y/V\) for a small \(V \subseteq Y\), the Gelfand numbers restrict \(S\) along the inclusion \(\iota _M : M \hookrightarrow X\) for a subspace \(M \subseteq X\) of small codimension. With \(M = X\) one gets \(c_0(S) = \| S\| \); (S2) is the triangle inequality applied to \((S+T) \circ \iota _M\). For the ideal property (S3), following [ 8 , § 2.4 ] , take admissible \(M\) for \(S\) and pass to \(M' := A^{-1}(M)\): it is closed, its codimension is at most that of \(M\) by the first isomorphism theorem applied to \(\pi _M \circ A\), and \(\| BSA(w)\| \le \| B\| \, \| S \circ \iota _M\| \, \| A\| \, \| w\| \) for \(w \in M'\). For (S4) take \(M := \ker S\), which is closed with \(\operatorname {codim} M = \operatorname {rank} S \le n\) and \(S \circ \iota _M = 0\). For (S5\('\)), the inclusion \(\iota _M\) is an isometry, so the identity restricted to any nontrivial \(M\) has norm \(1\), and \(\operatorname {codim} M \le n {\lt} \dim X\) forces \(M \neq \{ 0\} \). Formalised in Gelfand.lean.