A flat connection admits local parallel frames

Assume $\mathrm{\nabla }$ is flat, fix $p$, and take a coordinate ball $U$ from [F1], small enough to lie in one bundle trivialization. Let $v_1,\dots ,v_r$ be the basis of $E_p$ induced by that trivialization and define $e_a(q)=P_{p,q}{v}_a$, where [F1] makes the notation independent of the path in $U$. Using the radial coordinate paths, [F4] shows that $e_a$ depends smoothly on $q$. Linear ODE uniqueness makes transport linear, and transport along the reversed path is its inverse; hence the $e_a(q)$ form a basis of $E_q$ and [F3] makes $(e_a)$ a local frame.

For $q\in U$ and a smooth curve $c$ through $q$, concatenate any path from $p$ to $q$ with the segment of $c$. Endpoint independence in [F1] identifies $e_a(c(t))$ with parallel transport of $e_a(q)$ along $c$; [F2] therefore gives ${\mathrm{\nabla }}_{\dot{c}}{e}_a=0$. Every tangent vector is the velocity of such a local curve, so every $e_a$ is parallel. This proves the forward implication.

Conversely, suppose every point has a neighborhood with a parallel frame. On such a neighborhood the defining curvature commutator gives $R^{\mathrm{\nabla }}(X,Y)e_a=0$ because all three covariant derivatives of $e_a$ vanish. At each point the $e_a$ are a basis by [F3], so [F5] gives $R^{\mathrm{\nabla }}(X,Y)=0$ on the whole fibre. These neighborhoods cover $M$, hence the connection is flat.