The covering of a leaf associated with the holonomy kernel exists

The leaf is a nice base. By [F1] the leaf $L$ is a connected smooth manifold with its own manifold topology and smooth structure, the inclusion $L\hookrightarrow M$ being a connected injective immersion. By [F2] $L$ is path-connected, locally path-connected and semilocally simply connected. Hence by [F3] there is a universal cover $q:\tilde{L}\to L$ and the deck group $\mathrm{Deck}(q)$ is isomorphic to ${\pi }_1(L,x)$ via the assignment sending a loop class to the deck transformation moving a chosen point of the fibre over $x$ to the lifted endpoint. Fix $\tilde{x}$ over $x$; this fixes the isomorphism.

The subgroup acts by a covering-space action. The deck group acts on the connected total space $\tilde{L}$ by a covering-space action by [F4]. Restricting the action to the subgroup $K$ (under the isomorphism of step 1.1) preserves the defining property: a neighbourhood $U$ with $\gamma U\cap U=\mathrm{\varnothing }$ for all nonidentity $\gamma \in \mathrm{Deck}(q)$ also satisfies it for all nonidentity elements of $K$.

The intermediate covering. Let $q_K:\tilde{L}\to \widehat{L}:=\tilde{L}\mathrm{/}K$ be the orbit covering supplied by [F4]. Since $q$ is constant on $K$-orbits, it factors uniquely as $q=p\circ q_K$ through a continuous map $p:\widehat{L}\to L$. For a connected evenly covered coordinate neighborhood $W\subseteq L$, the sheets of $q^{-1}(W)$ are permuted by $K$. Each $K$-orbit of sheets projects under $q_K$ to one open set in $\widehat{L}$ mapped homeomorphically by $p$ onto $W$: choose one sheet to define its inverse, and the other sheets in its orbit give exactly the same quotient points. Distinct sheet orbits give disjoint sets. Thus $p$ is a covering. The space $\widehat{L}$ is path connected as the continuous image of the path-connected universal cover.

The image subgroup. Fix $\widehat{x}=q_K(\tilde{x})$. For a loop $a$ at $x$, let $\tilde{a}$ be its lift through $q$ starting at $\tilde{x}$. Its endpoint is $g\tilde{x}$, where $g$ is the deck transformation corresponding to $[a]$ by [F3]. Then $q_K\circ \tilde{a}$ is its lift through $p$, and this lift closes exactly when $q_K(g\tilde{x})=q_K(\tilde{x})$, equivalently $g\in K$, since the deck action is free. If $[a]\in p_{\ast }{\pi }_1(\widehat{L},\widehat{x})$, an upstairs representing loop and uniqueness of lifts show this lift closes. Conversely, a closed lift is an upstairs loop projecting to $a$. Hence $p_{\ast }{\pi }_1(\widehat{L},\widehat{x})=K$; injectivity of $p_{\ast }$ in [F5] also gives ${\pi }_1(\widehat{L},\widehat{x})\cong K$.

Uniqueness. Let $p^{\mathrm{\prime }}:{\widehat{L}}^{\mathrm{\prime }}\to L$ be a connected covering with image subgroup $K$ at a point ${\widehat{x}}^{\mathrm{\prime }}$ over $x$. Coverings of a locally path-connected manifold are locally path connected, so their connected total spaces are path connected. The lifting criterion [F5], applied to $p$ through $p^{\mathrm{\prime }}$ and to $p^{\mathrm{\prime }}$ through $p$, gives based maps $u:\widehat{L}\to {\widehat{L}}^{\mathrm{\prime }}$ and $v:{\widehat{L}}^{\mathrm{\prime }}\to \widehat{L}$ over $L$. The composites and the identities are based lifts of $p$ or $p^{\mathrm{\prime }}$ through the same covering, so uniqueness in the lifting criterion gives $vu=\mathrm{i}\mathrm{d}$ and $uv=\mathrm{i}\mathrm{d}$. Thus these coverings are isomorphic over $L$. If a different point over $x$ was originally chosen, choose a point at which its image subgroup is $K$, as required by the hypothesis.