Local systems correspond to group-ring modules

A connected CW complex is path connected. The image of each characteristic disk is path connected, so it lies in one path component. Hence every path component $P$ intersects each closed cell either in the whole cell or not at all. Both $P$ and its complement therefore have closed intersection with every closed cell, and the weak-topology test in [F5] makes both sets closed. Thus $P$ is also open; connectedness leaves only one path component. Consequently the set of paths $x\to y$ is nonempty for every $y\in X$. Use [F4] once to choose such a path $p_y$, taking $p_x=c_x$.

For a local system $\mathcal{L}$, give ${\mathcal{L}}_x$ the action in the statement. If $a,b$ are loop classes, covariance gives $T_{ab}=T_b{T}_a$ and hence $T_{\overline{ab}}=T_{\bar{a}}{T}_{\bar{b}}$; therefore $(ab)m=a(bm)$. Constants act identically and reversals act inversely. The operators are $R$-linear, so [F3] extends this action uniquely to an $R[{\pi }_1(X,x)]$-module. Naturality makes the component ${\eta }_x$ of every coefficient morphism equivariant. This defines the evaluation functor $E$.

Conversely let $M$ be a left $R[{\pi }_1(X,x)]$-module. Define a local system $Q(M)$ with every fiber equal to the underlying $R$-module $M$. For a path $\gamma :y\to z$, put ${\mathrm{\ell }}_{\gamma }=[p_y\ast \gamma \ast {\bar{p}}_z]\in {\pi }_1(X,x)$ and $Q(M)([\gamma ])(m)={\mathrm{\ell }}_{\gamma }^{-1}\cdot m$. Endpoint-fixed homotopies do not change ${\mathrm{\ell }}_{\gamma }$. Constants give the identity. If $\gamma :y\to z$ and $\delta :z\to w$, cancellation of ${\bar{p}}_z\ast p_z$ gives ${\mathrm{\ell }}_{\gamma \ast \delta }={\mathrm{\ell }}_{\gamma }{\mathrm{\ell }}_{\delta }$, so $Q(M)(\gamma \ast \delta )=({\mathrm{\ell }}_{\gamma }{\mathrm{\ell }}_{\delta }{)}^{-1}\cdot -={\mathrm{\ell }}_{\delta }^{-1}\cdot ({\mathrm{\ell }}_{\gamma }^{-1}\cdot -)=Q(M)(\delta )Q(M)(\gamma )$. Thus $Q(M)$ is a covariant functor. A module map, used on every fiber, is a natural transformation by equivariance; hence $Q$ is a functor.

Since $p_x$ is constant, for a loop $a$ at $x$ the action obtained by evaluating $Q(M)$ is $a\cdot m=Q(M)(\bar{a})m=a\cdot m$. Hence $EQ$ is literally the identity on modules and their maps. For a local system $\mathcal{L}$, define ${\epsilon }_y:Q(E\mathcal{L}{)}_y={\mathcal{L}}_x\to {\mathcal{L}}_y$ by ${\epsilon }_y=T_{p_y}$. The action on $E\mathcal{L}$ and the definition of $Q$ give $Q(E\mathcal{L})(\gamma )=T_{p_y\ast \gamma \ast {\bar{p}}_z}$. Therefore $T_{p_z}Q(E\mathcal{L})(\gamma )=T_{\gamma }{T}_{p_y}$, so $\epsilon$ is a natural isomorphism $QE\mathcal{L}\to \mathcal{L}$. It is natural in $\mathcal{L}$ because coefficient morphisms commute with every $T_{p_y}$.

Steps 1.2–3.1 exhibit the required equivalence. A second chosen path family produces another $Q^{\mathrm{\prime }}$ and the component $[p_y\ast {\bar{p}}_y^{\mathrm{\prime }}{]}^{-1}$ acting on $M$ gives the natural isomorphism $Q(M{)}_y\to Q^{\mathrm{\prime }}(M{)}_y$; the same cancellation as in step 2.1 proves naturality. Thus path choices affect the displayed model but not its natural-isomorphism class. The only AC use was the point-indexed family in step 1.1; for a one-point space only the constant path is needed, while the empty case is excluded by the chosen basepoint.