Cellular cochains compute cohomology with local coefficients

Apply the local-coefficient cohomological excision of [F5], using its simplexwise small-chain inverse, to the open-cell neighborhoods in the relative $m$-skeleton. A separated open $m$-cell has constant coefficients after transport from one point, and the relative disk-boundary cellular cochain complex has one copy of that fiber in degree $m$ and zero elsewhere. Hence $H^q(X^m\cup A,X^{m-1}\cup A;\mathcal{L})=0$ for $q\mathrm{\ne }m$, while the degree-$m$ group is the product of the dual cell-coordinate groups, precisely $C_{\mathrm{c}\mathrm{e}\mathrm{l}\mathrm{l}}^m(X,A;\mathcal{L})$.

In connected universal-cover coordinates, $g\cdot c=c\cdot g^{-1}$ makes the cellular boundary left $R[\pi ]$-linear and applying ${\mathrm{Hom}}_{R[\pi ]}(-,{\mathcal{L}}_x)$ gives the cellular coboundary by precomposition. Rewriting left equivariance at $c\cdot g=g^{-1}\cdot c$ gives $\phi (c\cdot g)=g^{-1}\phi (c)$, so every map is typed as claimed.

For the triple $X^{m-1}\cup A\subseteq X^m\cup A\subseteq X^{m+1}\cup A$, the connecting maps in [F3] compose to the cellular coboundary. Exactness and the concentration in step 1.1 give, by a direct kernel-image chase, $\ker d^n\mathrm{/}\mathrm{im}{d}^{n-1}\cong H^n(X^{n+1}\cup A,A;\mathcal{L})$. Attaching cells in dimensions above $n+1$ leaves this group unchanged because the two adjacent relative groups vanish.

For an infinite CW complex, use the telescope in [F4] and split it into alternating closed skeletal cylinders with overlapping half-cylinders. The local cochain Mayer--Vietoris sequence of [F5], applied to interiors of these cylinder neighborhoods, gives the exact sequence for this cover. The pieces are disconnected unions. By [A1], a family of componentwise cocycles is a coboundary in their product complex exactly when one may choose a primitive in every component; hence the cohomology of each piece is the product of the cohomologies of its skeletal components. Retraction of the pieces onto the skeleta then identifies the Mayer--Vietoris product map with $\mathrm{\Delta }:{\prod }_m{H}^q(X^m,A^m;\mathcal{L})\to {\prod }_m{H}^q(X^m,A^m;\mathcal{L})$, where $\mathrm{\Delta }((a_m){)}_m=a_m-i_m^{\ast }{a}_{m+1}$. Step 2.1 says that both the degree-$n$ and degree-$(n-1)$ inverse systems are eventually constant with isomorphism transition maps. For any eventually constant system, $\ker \mathrm{\Delta }$ is its stable value, while $\mathrm{\Delta }$ is onto: set the first stable-tail coordinate to zero, recurse forward there through the inverse transition maps, and then recurse through the finitely many earlier coordinates toward zero. Exactness therefore identifies $H^n$ of the telescope with the stable value $H^n(X^{n+1}\cup A,A;\mathcal{L})$. Pair homotopy invariance from [F4] identifies this with $H^n(X,A;\mathcal{L})$, with no inverse-limit remainder.

A cellular map preserves the skeletal triples and their connectors, and [F3] makes the restriction maps natural for a coefficient morphism $f^{\ast }\mathcal{K}\to \mathcal{L}$. The telescope splitting and the map $\mathrm{\Delta }$ are natural as well. Therefore the identifications in steps 1.1--3.1 commute with induced cochain maps. Empty pairs, no cells, zero systems/rings, degree zero, negative degrees, and disconnected products are all covered by the same componentwise exact chase. AC is used only in Step 3.1 to assemble componentwise primitives.