  Let \(\Phi(X)\) be the formula \(X \approx U \vee X \approx V\). Then clearly we may assert \(\forall X[\Phi(X) \rightarrow \exists xX(x)]\) so AC1L may be invoked to assert \(\exists F \forall X[\Phi(X) \rightarrow X(FX)]\). Now we can introduce a function constant \(K\) together with the assertion