A represented-path composition used by incoming-arrow sums

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.biproductProjection_pathRepresentableMap_comp_arrow {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {z x y : Q} (p : Quiver.Path z x) (a : x ⟶ y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π P.quotientRepresentable (obj P.relations z)) (P.pathRepresentableMap p)) (P.arrowRepresentableMap a) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π P.quotientRepresentable (obj P.relations z)) (P.pathRepresentableMap (p.cons a))

Precomposing the path-representable composition law by the relevant biproduct projection gives the literal continuation/path equality.