The paper contains quite a number of interesting results, which in their simplest form read as follows. Suppose we are given a proof in WE- \(\text{PA}^ \omega+\)AC-qf of \(\forall x^ 1 \forall\widetilde x\leq_ \rho sx \exists y^ \tau A_ 0\) with \(A_ 0\) quantifier-free, \(s\) a closed term of Gödel’s \(T\) and \(\tau\leq 2\). Then one can extract a closed term \(\Phi\in T\) such that WE-\(\text{HA}^ \omega\lvdash\forall x^ 1 \forall\widetilde x\leq_ \rho sx \exists y\leq_ \tau \Phi x A_ 0\). This result is obtained by a combination of functional interpretation and a pointwise version of hereditary majorization of functionals from \(T\). One of the generalizations dealt with in the paper allows additional assumptions of the form \(\forall x^ \delta \exists y\leq_ \rho sx \forall z^ \eta A_ 0\). The author shows (by an adaptation of a well- known counterexample due to Kreisel) that a straightforward generalization of his method to proofs of weak König’s Lemma WKL fails. However, it turns out that one can construct an equivalent WKL\('\) of WKL (in \(\widehat{\text{WE-}\text{HA}}^ \omega \upharpoonright\)) which has the right logical form for an admissible premise: \(\forall f^ 1\), \(g^ 1 \exists b\leq_ 1 \lambda k 1 \forall x^ 0(\widehat{(\hat f)_ g}(\bar b x)=_ 0 0)\). Therefore the previous results generalize to proofs using WKL. As a corollary, some new conservation results for WKL are derived, e.g. with respect to sentences of the form \(\forall u^ 1\forall v\leq tu \exists w^ \eta B_ 0\). The particular logical form of the sentences considered is motivated by intended applications to uniqueness theorems in approximation theory, which the author plans to elaborate in subsequent papers. – The paper is an extended version of parts of the author’s dissertation (thesis adviser: H. Luckhardt).