A based morphism between connected coverings exists exactly when the induced subgroups are included

For the forward implication, [F7] applied to $p_2\circ f=p_1$ gives the displayed subgroup inclusion. For the reverse implication, [F2] makes $E_1$ locally path-connected and [F5] makes it path-connected. Apply [F1] to the map $p_1:E_1\to B$ and the covering $p_2:E_2\to B$; the inclusion produces a based lift $f:E_1\to E_2$, and $p_{2}f=p_1$ says exactly that it is a map of coverings.

Uniqueness is part of [F1], and also follows from [F3] because any two such maps lift $p_1$ and agree at $e_1$.

First, $f$ is surjective. Indeed, [F2] and [F5] make $E_2$ path-connected. Join $f(e_1)$ to any $z\in E_2$ by a path, project that path through $p_2$, and lift the projection through $p_1$ from $e_1$. The image of this lift under $f$ is a lift with the original initial point, so uniqueness in [F6] makes it the original path and its endpoint maps to $z$. Now fix $b\in B$. Intersect evenly covered neighbourhoods of $b$ for $p_1$ and $p_2$, then use local path-connectedness to choose a path-connected open neighbourhood $O$ inside that intersection. For a $p_1$-sheet $U$ over $O$, choose $x\in U$ and let $V$ be the $p_2$-sheet containing $f(x)$. The maps $f{\mathrm{\mid }}_U$ and $(p_2{\mathrm{\mid }}_V{)}^{-1}\circ p_1{\mathrm{\mid }}_U$ are lifts of $p_1{\mathrm{\mid }}_U$ through $p_2$, agree at $x$, and have connected domain $U$; hence [F3] makes them equal. Thus $f{\mathrm{\mid }}_U:U\to V$ is a homeomorphism. Conversely, every point of $f^{-1}(V)$ lies in one such $U$. Hence $f^{-1}(V)$ is the disjoint union of exactly those $p_1$-sheets sent to $V$, each mapped homeomorphically onto $V$. Surjectivity makes this family nonempty for every $V$, so every point of $E_2$ has an evenly covered neighbourhood and [F4] makes $f$ a covering map.