Fundamental cycles of a spanning tree generate all flows

Let $V$ and $E$ be finite types with decidable equality, and let $hd, tl : E \to V$ be two maps, to be read as the head and tail of each edge of a finite directed multigraph, so that $e$ runs from $tl\,e$ to $hd\,e$. Let $T$ be a finite set of edges, and assume the spanning-tree hypothesis in the following form: for every pair of vertices $u, v$ there is exactly one $c : E \to \mathbb{Z}$ supported on $T$ (that is, $c\,e = 0$ for all $e \notin T$) whose divergence at each vertex $w$, namely $\sum_{e : hd\,e = w} c\,e - \sum_{e : tl\,e = w} c\,e$, equals $[w = v] - [w = u]$. The conclusion asserts the existence of $Z : E \to E \to \mathbb{Z}$ such that: (i) for every index $j$, the chain $Z\,j$ is a circulation, i.e. $\sum_{e : hd\,e = w} Z\,j\,e = \sum_{e : tl\,e = w} Z\,j\,e$ at every vertex $w$; (ii) for $j, j'$ in the complement $T^{c}$ one has $Z\,j\,j' = 1$ if $j = j'$ and $0$ otherwise; (iii) $Z\,j = 0$ for $j \in T$; and (iv) for every additive commutative group $A$ and every $f : E \to A$ satisfying the balance condition $\sum_{e : hd\,e = w} f\,e = \sum_{e : tl\,e = w} f\,e$ at every vertex $w$, one has $f\,e = \sum_{j \in T^{c}} Z\,j\,e \cdot f\,j$ for every edge $e$, the coefficients acting through the $\mathbb{Z}$-module structure of $A$.

This is the classical statement that the fundamental cycles attached to the edges outside a spanning tree span the cycle space of a finite directed multigraph, here formulated for flows with values in an arbitrary abelian group: such a flow is determined, with universal integer coefficients, by its values on the non-tree edges. It is used in the construction of path integrals on curves, in AlgebraicCurve.exists_loops_pathIntegral_reciprocity_raw and in CerednikDrinfeld.Omega.exists_isUnit_det_pathCycle_and_span_pathCycle.