A compact compact-open family is equicontinuous on a locally compact Hausdorff domain

If $X=\mathrm{\varnothing }$ or $\mathcal{K}=\mathrm{\varnothing }$, the conclusion is vacuous. Otherwise fix $x\in X$ and $\epsilon >0$.

Call a pair $(O,U)$ of open sets admissible at $f\in \mathcal{K}$ when $f\in O$, $x\in U$, and $d(g(y),f(x))<\epsilon \mathrm{/}3$ for every $g\in O$ and every $y\in U$. Continuity of evaluation at $(f,x)$, which [L1] supplies, makes at least one pair admissible at each $f\in \mathcal{K}$. Let $\mathcal{A}$ be the set of all triples $(f,O,U)$ with $(O,U)$ admissible at $f$. This set is defined outright and no pair is selected, so no choice principle is used.

The open sets $O$ occurring in triples of $\mathcal{A}$ cover $\mathcal{K}$, because each $f\in \mathcal{K}$ lies in the $O$ of some admissible triple. Applying [L2] to the cover indexed by $\mathcal{A}$ yields finitely many triples $(f_1,O_1,U_1),\dots ,(f_m,O_m,U_m)$ of $\mathcal{A}$ whose $O_i$ already cover $\mathcal{K}$; only this finite selection is made. Put $U=U_1\cap \cdots \cap U_m$, an open neighbourhood of $x$ as a finite intersection.

Let $g\in \mathcal{K}$ and take $i\le m$ with $g\in O_i$. If $y\in U$ then $y\in U_i$ and $x\in U_i$, so admissibility at $f_i$ gives $d(g(y),f_i(x))<\epsilon \mathrm{/}3$ and $d(g(x),f_i(x))<\epsilon \mathrm{/}3$, whence $d(g(y),g(x))<2\epsilon \mathrm{/}3<\epsilon$. The one neighbourhood $U$ works for every $g\in \mathcal{K}$, which is what [L3] requires for equicontinuity at $x$.