On a connected covering space, a deck transformation is determined by one point and the deck action is free

Given: The objects, hypotheses, and choice principles stated above.

For a covering $p:E\to B$, a deck transformation is an isomorphism $h:E\to E$ over $B$, so $p\circ h=p$ (def-map-and-isomorphism-of-covering-spaces). Deck transformations form the deck group $\mathrm{Deck}(p)$ under composition, and this group acts on $E$ by evaluation (def-group, def-group-action). (Deck transformations and the deck-transformation group of a covering).

Let $Y$ be connected and let $f,g:Y\to E$ be lifts through the same covering of the same map $Y\to B$. If $f(y_0)=g(y_0)$ for some $y_0\in Y$, then $f=g$. (Two lifts from a connected space that agree at one point agree everywhere).

A left action of a group $G$ on a set $X$ (def-group-action) is free when $g\cdot x=x⟹g=e$ for every $g\in G$ and $x\in X$. Equivalently, no nonidentity element of $G$ fixes any point of $X$. (A free group action has no nonidentity element fixing a point).