The image of one incoming-arrow continuation vector

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.incomingArrowRangeSumKLinearMap_singleBasis {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) (y : Q) (a : DisplayedIncomingArrow y) (p : P.LeftContinuationPath a.snd) : (P.incomingArrowRangeSumKLinearMap y) (P.incomingArrowRangeSingle y a ((P.incomingArrowModuleBasisFamily y a) p)) = P.representedPathElement y ↑((P.incomingContinuationEquivPositiveVertexPath y) ⟨a, p⟩)

The incoming-range sum sends the basis continuation in one arrow coordinate to the represented path obtained by adjoining that arrow.