The line integral of a continuous function admitting a primitive is that primitive's endpoint increment along every rectifiable path

Fix $\epsilon >0$. For a point $p$ of the trace let $S_p$ be the set of $r\in (0,1]$ such that $B(p,r)$ lies in the open domain and $\mathrm{\mid }f(u)-f(p)\mathrm{\mid }<\epsilon \mathrm{/}2$ for every $u\in B(p,r)$. Continuity of $f$ at $p$ and openness of the domain make $S_p$ nonempty, and $S_p$ is downward closed in $(0,1]$, so $r_p:=\frac{1}{2}\sup S_p$ is a positive real belonging to $S_p$; the assignment $p\mapsto r_p$ is defined outright, not selected, so no choice principle is used. The balls $B(p,r_p)$ cover the compact trace by [L6], so [L7] supplies $\delta >0$ such that any two trace points at distance below $\delta$ lie in a single $B(p,r_p)$. That ball is convex, so the segment joining them stays inside it, and $\mathrm{\mid }f(u)-f(z)\mathrm{\mid }<\epsilon$ all along that segment.

For trace points $z,w$ as in step 1.1, apply [L4] componentwise to the straight segment and then [L8] to $f-f(z)$. This gives $F(w)-F(z)=f(z)(w-z)+r(z,w)$ with $\mathrm{\mid }r(z,w)\mathrm{\mid }\le \epsilon \mathrm{\mid }w-z\mathrm{\mid }$.

By [L6] and [L10], choose $\eta >0$ so that every partition with mesh below $\eta$ has consecutive trace points within $\delta$. For every such partition, sum the identity of step 2.1: the left side telescopes to $F(\gamma (b))-F(\gamma (a))$, and by [L2] and repeated use of [L9] the total remainder is at most $\epsilon L(\gamma )$. As the mesh tends to $0$, [L5] identifies the limit of the main sums with the complex integral, so $\mathrm{\mid }F(\gamma (b))-F(\gamma (a))-{\int }_{\gamma }fdz\mathrm{\mid }\le \epsilon L(\gamma )$.

Letting $\epsilon \downarrow 0$ proves the formula for every rectifiable contour. The argument also covers constant paths, for which [L2] gives length $0$ and both sides vanish.