The 1-skeleton of a connected CW complex is connected: attaching a cell of dimension at least two has connected attaching sphere, so it cannot join two components of the preceding skeleton. Since $K$ is finite, its 1-skeleton is a finite connected graph. The unique paths in $T$ contract it to $v_0$, supplying the contraction required by [F2]. The quotient that collapses $T$ to a point is a wedge with one circle for each 1-cell outside $T$, and [F3] gives the free basis represented by the loops $x_e$.

Suppose a 2-cell is attached to a path-connected finite subcomplex $X$ along $\alpha :S^1\to X$. In the attached space, the open sets consisting of $X$ together with an outer collar of the disk and the inner open disk cover the space; the first retracts to $X$, the second is contractible, and their overlap is an annulus retracting to $S^1$. Choose a basepoint on that annulus and connect it to $v_0$ and to the attaching basepoint by the collar and a path in $X$. Under the retraction to $X$, the once-around generator of the annulus maps to the resulting based attaching loop $\gamma \ast \alpha \ast \bar{\gamma }$; in the inner disk it maps to the identity. By [F4] and [F5], the pushout therefore imposes exactly that loop as a relation. The quotient by its normal closure has the same universal property: a homomorphism out of it is precisely a homomorphism out of ${\pi }_1(X,v_0)$ that sends the based attaching loop to the identity.

Attaching the finitely many 2-cells one at a time therefore quotients the free group from step 1.1 by the normal closure of all the words $r_f$. Replacing a connecting path conjugates the corresponding based loop, so its normal closure is unchanged.

If an $n$-cell with $n\ge 3$ is attached, the same collar cover has overlap homotopy equivalent to $S^{n-1}$. For $m\ge 2$, the sphere $S^m$ is covered by the complements of two antipodal points; both sets are contractible and their overlap $S^{m-1}\times \mathbb{R}$ is path-connected. [F4] therefore gives ${\pi }_1(S^m)=1$. Applying [F4] to the cell-attachment cover shows that attaching the $n$-cell induces an isomorphism on fundamental groups.

Attaching every higher-dimensional cell preserves the group from step 2.1. The finite presentation in the Statement follows, including the cases with no non-tree edges or no 2-cells.

The relation is reflexive because $H(s,t)=\gamma (t)$ has rank at most one and fixed endpoints; subdivide the square along each breakpoint of a finite smooth partition of $\gamma$ and triangulate the resulting strips. It is symmetric by replacing $s$ with $1-s$ and reflecting a witnessing subdivision. For transitivity, first take finite common refinements of the boundary subdivisions of $H_0$ and $H_1$ along their common path ${\gamma }_1$, then paste $H_0(2s,t)$ on $0\le s\le \frac{1}{2}$ to $H_1(2s-1,t)$ on $\frac{1}{2}\le s\le 1$. The common boundary is the same path ${\gamma }_1$, so this paste is continuous; the scaled finite subdivisions on the two halves give a finite curvilinear-triangle subdivision after triangulating any resulting polygons. It fixes both path endpoints, and its differential has rank at most one on each triangle. Thus the relation is an equivalence relation.

If ${\gamma }_0{\sim }_{\mathrm{t}\mathrm{h}\mathrm{i}\mathrm{n}}{\gamma }_1$ and ${\delta }_0{\sim }_{\mathrm{t}\mathrm{h}\mathrm{i}\mathrm{n}}{\delta }_1$ with matching endpoints, paste their homotopies on the first and second halves of the path parameter, scaling their finite subdivisions to those halves and taking a finite common refinement along their shared fixed endpoint. The shared endpoint is fixed throughout each homotopy, so the paste is continuous and piecewise smooth; on each triangle its differential has image contained in that of the corresponding homotopy differential, hence rank at most one. Therefore ${\delta }_0\ast {\gamma }_0{\sim }_{\mathrm{t}\mathrm{h}\mathrm{i}\mathrm{n}}{\delta }_1\ast {\gamma }_1$, and composition of classes is well-defined.

Let $\mathrm{\Gamma }$ be the path obtained by placing the three given paths, in order, on the three consecutive thirds of $[0,1]$. Each parenthesized concatenation is $\mathrm{\Gamma }\circ {\varphi }_j$ for an increasing piecewise-linear homeomorphism ${\varphi }_j:[0,1]\to [0,1]$. Put $u(s,t)=(1-s){\varphi }_0(t)+s{\varphi }_1(t)$ and $H(s,t)=\mathrm{\Gamma }(u(s,t))$. Refine the $t$-partition by all breakpoints of ${\varphi }_0$ and ${\varphi }_1$. On each resulting strip $u$ is smooth and piecewise bilinear. For every breakpoint $b$ of the piecewise-smooth path $\mathrm{\Gamma }$, also subdivide along the level set $u^{-1}(b)$; on each strip these finitely many level sets are smooth arcs, with their finitely many endpoints and intersections included in the subdivision. The resulting regions have finitely many smooth boundary arcs and can be triangulated into curvilinear triangles. On each triangle, $u$ remains in one smooth piece of $\mathrm{\Gamma }$, so $H$ is smooth there and both differential columns are scalar multiples of the single vector ${\mathrm{\Gamma }}^{\mathrm{\prime }}$. Its rank is at most one. Thus the two parenthesizations are thin-homotopic. For the right identity law use ${\rho }_0(t)=2t$ on $[0,\frac{1}{2}]$ and ${\rho }_0(t)=1$ on $[\frac{1}{2},1]$, with ${\rho }_1(t)=t$; for the left identity law use ${\rho }_0(t)=0$ on $[0,\frac{1}{2}]$ and ${\rho }_0(t)=2t-1$ on $[\frac{1}{2},1]$, again with ${\rho }_1(t)=t$. The corresponding homotopies $\gamma ((1-s){\rho }_0(t)+s{\rho }_1(t))$ have the required concatenated and unaltered paths as boundaries. Refine each square along the parameter-map breakpoints and the preimages of every breakpoint of $\gamma$; any region on which the argument is constant is already smooth. The same rank argument proves both identity laws.

Put $\lambda (t)=2t$ for $0\le t\le \frac{1}{2}$ and $\lambda (t)=2(1-t)$ for $\frac{1}{2}\le t\le 1$. Then $t\mapsto \gamma (\lambda (t))$ traverses $\gamma$ and then its reverse. The map $H(s,t)=\gamma ((1-s)\lambda (t))$ joins this path to the constant path at $\gamma (0)$ with both endpoints fixed. Subdivide first at $t=\frac{1}{2}$, then along the preimages of every breakpoint of a finite smooth partition of $\gamma$ under $(s,t)\mapsto (1-s)\lambda (t)$; these are finitely many smooth arcs or constant regions on the two parameter strips. Triangulating the resulting finite curvilinear regions makes $H$ smooth on each triangle. Its differential has rank at most one because both derivatives are scalar multiples of $\dot{\gamma }$. Applying the same construction to $\bar{\gamma }$ contracts the reverse-then-forward path at $\gamma (1)$. Hence $[\bar{\gamma }]$ is a two-sided inverse of $[\gamma ]$.

The tagged morphism set has well-defined domain and codomain by construction; step 2.1 makes composition independent of representatives, step 3.1 gives associativity, and step 3.2 gives the inverse axiom. Steps 3.1 and 3.2 also provide the two identity laws stated in [F3]. Thus the data form a category in which every morphism is invertible, which is a groupoid by [F4].

The map $f(x,y)=x^2+y^2$ has derivative $(2x,2y)$, which is nonzero on $f^{-1}(1)$; thus $1$ is a regular value and [F2] makes $S^1$ a smooth one-dimensional submanifold. Let $\tilde{\alpha }=xdy-ydx$ be the ambient one-form on ${\mathbb{R}}^2$, let $\iota :S^1\hookrightarrow {\mathbb{R}}^2$ be inclusion, and put $\alpha ={\iota }^{\ast }\tilde{\alpha }$, which is defined by [F8] and smooth by [F9]. The global tangent field $X=(-y,x){\mathrm{\mid }}_{S^1}$ spans each tangent line and satisfies $\alpha (X)=x^2+y^2=1$. By [F10], $d\alpha$ is a smooth two-form. By [F4], $d\alpha (X,X)=X(\alpha (X))-X(\alpha (X))-\alpha ([X,X])=0$; since $X$ spans each one-dimensional tangent space, this gives $d\alpha =0$ intrinsically on $S^1$. Along $\gamma$, $\dot{\gamma }(t)=2\pi X_{\gamma (t)}$, so [F6] gives ${\int }_{\gamma }\alpha ={\int }_0^{1}2\pi dt=2\pi$; the constant loop has integral zero.

Suppose a thin homotopy $H:[0,1{]}^2\to S^1$ joined $\gamma$ to the constant loop while fixing the basepoint at the path endpoints. Parametrize every curvilinear triangle in its finite subdivision by the specified smooth map from the standard two-simplex and compose that parametrization with $H$. By the smooth-up-to-boundary convention of Piecewise-smooth paths and thin homotopies, each composition has a smooth extension to a neighborhood of the standard simplex, so it is a smooth singular simplex by [F7]. Orient these finitely many simplices compatibly with the square and apply [F5] to each, then add the formulas. Each shared geometric edge occurs twice with opposite orientations. Choose one smooth reference parametrization $\sigma$ for such an edge; the two oriented face restrictions are $\sigma \circ \varphi$ and the reverse of $\sigma \circ \psi$, for increasing smooth reparametrizations $\varphi ,\psi :[0,1]\to [0,1]$. By [F6] and one-variable substitution, their oriented integrals are ${\int }_{\sigma }\alpha$ and $-{\int }_{\sigma }\alpha$, so they cancel. The remaining terms are exactly the oriented square boundary under $H$. Step 1.1 gives $d\alpha =0$, hence Stokes gives zero for the total boundary integral. The two path edges have signed integral $2\pi$ or $-2\pi$ because one is $\gamma$ and the other is constant; the endpoint edges are constant and contribute zero. Thus the boundary integral is $\pm 2\pi \mathrm{\ne }0$, a contradiction. Therefore $[\gamma ]$ is not the identity class.

Apply [F1] on $[t_0,t_1]$ with initial matrix $I_n$ to obtain the unique $C^1$ solution on the first interval.

For each $j=2,\dots ,m$, apply [F1] on $[t_{j-1},t_j]$ with initial value equal to the terminal value already constructed at $t_{j-1}$. Adjacent solutions agree at their shared endpoint by construction, so the finite family pastes to a continuous piecewise-$C^1$ solution on $[0,1]$.

Any other such function has initial value $I_n$ on the first interval, so it agrees there by [F1]. If it agrees through $t_{j-1}$, then it has the same initial value as the constructed solution on the $j$th interval, so [F1] makes them agree there. Induction through the finite partition proves uniqueness on all of $[0,1]$.

On one closed curvilinear triangle $\mathrm{\Delta }$ of the subdivision, pull the connection back by the smooth restriction of $H$ and write its two coefficient matrices as $A_s=\omega (H_s)$ and $A_t=\omega (H_t)$. For a smooth family of paths inside $\mathrm{\Delta }$, let $U_t=-A_{t}U$, $U(s,0)=I$, and put $K=U_s+A_{s}U$. Smooth dependence in [F4] permits this differentiation, and [F5] gives uniqueness for the linear equation satisfied by $K$. The product rule gives $K_t+A_{t}K=-({\mathrm{\partial }}_s{A}_t-{\mathrm{\partial }}_t{A}_s+[A_s,A_t])U=-H^{\ast }F({\mathrm{\partial }}_s,{\mathrm{\partial }}_t)U$. Here [F3] identifies the pulled-back two-form as the curvature of the supplier connection.

Since $\mathrm{rank}(dH)\le 1$ on $\mathrm{\Delta }$, $H_s,H_t$ are linearly dependent and the alternating two-form satisfies $H^{\ast }F({\mathrm{\partial }}_s,{\mathrm{\partial }}_t)=F(H_s,H_t)=0$. Fix a vertex $q_0$ and join it to each $q\in \mathrm{\Delta }$ by the image of the straight radial path in the standard-simplex parametrization. The associated transports $Q(q)$ exist globally by [F5] and depend smoothly on $q$: apply [F4] locally in the endpoint parameter and continue over finitely many subintervals of the compact path interval, using uniqueness on overlaps. For each radial path, [F3] and the ODE give $(Q^{\mathsf{T}}\eta Q{)}^{\mathrm{\prime }}=0$, hence $Q(q{)}^{\mathsf{T}}\eta Q(q)=\eta$ and $Q(q)$ is invertible. Step 1.1 on this radial family with fixed start gives $dQ=-H^{\ast }\omega Q$. Thus transport from $q_1$ to $q_2$ in $\mathrm{\Delta }$ is $Q(q_2)Q(q_1{)}^{-1}$ by [F5], and the triangle boundary transport is identity.

The finite curvilinear-triangle subdivision is a finite connected CW complex $K$; choose the lower-left corner as basepoint and a maximal tree in its one-skeleton. The outer boundary loop contracts to that basepoint by the straight-line contraction of the parameter square, so [F6] makes its fundamental-group class the identity. By [F7], ${\pi }_1(K)$ has generators given by non-tree edge loops closed along the tree and relators given by based triangular face boundaries. For each free generator $x_e$, assign the inverse transport of its based edge loop and extend to a homomorphism $\mathrm{\Phi }$ from the free group; [F2]'s path-composition law gives $\mathrm{\Phi }(w)=U_w^{-1}$ for every edge word $w$. These transports are invertible because along each segment [F3] and the ODE give $(U^{\mathsf{T}}\eta U{)}^{\mathrm{\prime }}=-U^{\mathsf{T}}({\omega }^{\mathsf{T}}\eta +\eta \omega )U=0$, hence $U^{\mathsf{T}}\eta U=\eta$; reversing the ODE gives $U_{\bar{\alpha }}=U_{\alpha }^{-1}$. A based face relator is a tree path, a triangular boundary and the reverse tree path, so step 2.1 makes its transport and its $\mathrm{\Phi }$-image the identity. The boundary word is identity in the presentation by [F6]–[F8], and [F9] writes it as a finite product of conjugates of face relators and their inverses; all of these map to $I$, so $U_{\lambda }=I$. The side edges of the square are constant by fixed endpoints, giving $U_{\lambda }=U_{{\gamma }_1}^{-1}{U}_{{\gamma }_0}$ and $U_{{\gamma }_0}(1)=U_{{\gamma }_1}(1)$.

On the constant path the coefficient $\omega (\dot{\gamma })$ is zero, so the unique solution is $U(t)=I$. If $\gamma$ is followed by $\delta$, solve on the two parameter intervals with the terminal value from the first interval as initial value for the second. The second solution is $U_{\delta }(t)U_{\gamma }(1)$, so uniqueness gives $U_{\delta \ast \gamma }(1)=U_{\delta }(1)U_{\gamma }(1)$.

Write $\eta =\mathrm{diag}(-1,1,1,1)$. Along each smooth segment the derivative is $\frac{d}{dt}(U^{\mathsf{T}}\eta U)=U^{\mathsf{T}}(-{\omega }^{\mathsf{T}}\eta -\eta \omega )U=0$ by [F4]; continuity across the finite segment endpoints gives $U(t{)}^{\mathsf{T}}\eta U(t)=\eta$ throughout. Since $\eta$ is nonsingular, each $U(t)$ is invertible.

Let $U(t)$ solve along $\gamma$. The matrix $V(s):=U(1-s)U(1{)}^{-1}$ starts at $I$ and, since $\dot{\bar{\gamma }}(s)=-\dot{\gamma }(1-s)$, satisfies $V^{\mathrm{\prime }}(s)=-\omega (\dot{\bar{\gamma }}(s))V(s)$. Hence uniqueness gives $U_{\bar{\gamma }}(1)=U(1{)}^{-1}$. By [F3], transport is independent of the representative of a thin class; [F1]–[F2] and the identities in steps 1.1–1.2 therefore give well-defined component maps on the thin path groupoid.

For $[\gamma ]:x\to y$ and $[\delta ]:y\to z$, the associated tangent arrows compose as $(E_z{U}_{\delta }{E}_y^{-1})\circ (E_y{U}_{\gamma }{E}_x^{-1})=E_z{U}_{\delta }{U}_{\gamma }{E}_x^{-1}=E_z{U}_{\delta \ast \gamma }{E}_x^{-1}$ by step 1.1. Constant paths give identity tangent maps, and reversed paths give inverse tangent maps by step 2.1. Thus the stated object and arrow assignments define a functor into $\mathcal{T}(U)$ by [F6], with arrows in the stated groupoid by [F5].

Put $\tilde{U}(t)=\mathrm{\Lambda }(\gamma (t))U(t)\mathrm{\Lambda }(\gamma (0){)}^{-1}$. Differentiating and using $U^{\mathrm{\prime }}=-\omega (\dot{\gamma })U$ gives ${\tilde{U}}^{\mathrm{\prime }}(t)=(d\mathrm{\Lambda }(\dot{\gamma }){\mathrm{\Lambda }}^{-1}-\mathrm{\Lambda }\omega (\dot{\gamma }){\mathrm{\Lambda }}^{-1})\tilde{U}(t)=-{\omega }^{\mathrm{\prime }}(\dot{\gamma })\tilde{U}(t)$ by the transformation law [F4]. Its initial value is $I$, so uniqueness identifies $\tilde{U}$ with transport in the changed frame and gives the endpoint formula. Since $E_x^{\mathrm{\prime }}=E_x\mathrm{\Lambda }(x{)}^{-1}$, the corresponding tangent map is frame independent: $E_y^{\mathrm{\prime }}{U}_{\gamma }^{\mathrm{\prime }}(1)(E_x^{\mathrm{\prime }}{)}^{-1}=E_y{U}_{\gamma }(1)E_x^{-1}\mathrm{.}$ This is a local frame covariance statement; it is a principal-bundle gauge action only when $\mathrm{\Lambda }$ has the global extension required by the cited gauge-group definition.

Set $A={\omega }_i(p)$ and $B={\omega }_j(p)$. The integral equation $U(t)=I-{\int }_0^t\omega (\dot{\gamma })U$ gives the positive-$i$ segment expansion $S_1=I-\epsilon A+\frac{1}{2}{\epsilon }^2(A^2-{\mathrm{\partial }}_{i}A)+O({\epsilon }^3)$. On the following positive-$j$ segment, Taylor expansion at $p+\epsilon e_i$ gives $S_2=I-\epsilon B+{\epsilon }^2(\frac{1}{2}{B}^2-{\mathrm{\partial }}_{i}B-\frac{1}{2}{\mathrm{\partial }}_{j}B)+O({\epsilon }^3)$. In each case the second iterated integral contributes $\frac{1}{2}{\epsilon }^2{\omega }_k(p{)}^2$, and the first integral contributes the displayed derivative terms.

Along the negative-$i$ segment from $p+\epsilon e_i+\epsilon e_j$ to $p+\epsilon e_j$ and the negative-$j$ segment from $p+\epsilon e_j$ to $p$, the same integral expansion gives $S_3=I+\epsilon A+{\epsilon }^2(\frac{1}{2}{A}^2+\frac{1}{2}{\mathrm{\partial }}_{i}A+{\mathrm{\partial }}_{j}A)+O({\epsilon }^3)$ and $S_4=I+\epsilon B+\frac{1}{2}{\epsilon }^2(B^2+{\mathrm{\partial }}_{j}B)+O({\epsilon }^3)$. The derivative terms use starting points $p+\epsilon e_j$ and $p$; reversing the tangent changes the first-order ODE coefficient's sign.

For any fixed $q$, uniqueness in [F1] shows that adjoining a segment with identity-initial transport $S$ to an already traversed path with transport $T$ gives total matrix $ST$: $S(t)T$ solves the next segment's ODE with its required initial value. Applying this successively gives total transport $S_4{S}_3{S}_2{S}_1$; for $q=4$ this agrees with [F3] using the same component ODE of [F4]. Its linear terms cancel. The within-segment quadratic terms sum to $A^2+B^2-{\mathrm{\partial }}_{i}B+{\mathrm{\partial }}_{j}A$; the six cross-products sum to $BA-B^2-BA-AB-A^2+BA=BA-AB-A^2-B^2$. The full coefficient is therefore ${\mathrm{\partial }}_{j}A-{\mathrm{\partial }}_{i}B+BA-AB=-({\mathrm{\partial }}_i{\omega }_j-{\mathrm{\partial }}_j{\omega }_i+[A,B])=-F_{ij}(p)$ by [L1]. In the smooth tetrad specialization, evaluating $d\omega +\omega \wedge \omega$ on the commuting coordinate vectors gives exactly this expression, since $d\omega ({\mathrm{\partial }}_i,{\mathrm{\partial }}_j)={\mathrm{\partial }}_i{\omega }_j-{\mathrm{\partial }}_j{\omega }_i$ and $(\omega \wedge \omega )({\mathrm{\partial }}_i,{\mathrm{\partial }}_j)={\omega }_i{\omega }_j-{\omega }_j{\omega }_i$, in agreement with [F2]. For a uniform remainder, choose a compact neighborhood $K^{\mathrm{\prime }}$ of $K$ contained in $V$ and containing the four square sides for $0<\epsilon <{\epsilon }_0$; the $C^2$ coefficients and derivatives are bounded there. Taylor remainders in single integrals are uniformly $O({\epsilon }^3)$; replacing either coefficient in the second iterated integral by its value at $p$ also incurs $O({\epsilon }^3)$, since each coefficient differs by $O(\epsilon )$ over these length-$\epsilon$ sides. If $M$ bounds coefficient norms in the fixed submultiplicative norm, iterated-integral terms of order $m\ge 3$ are bounded by $M^m{\epsilon }^m\mathrm{/}m!$, whose sum is $O({\epsilon }^3)$. Multiplying four expansions preserves the uniform remainder order.