Covariant derivatives commute up to curvature in a two parameter variation

Fix any point in the parameter rectangle and choose a target coordinate chart near its image. Write $F=(x^a(s,t))$, $V=V^i(s,t){\mathrm{\partial }}_i$, $S=F_s$, and $T=F_t$; by [F2], $D_{t}V=({\mathrm{\partial }}_t{V}^i){\mathrm{\partial }}_i+V^i{D}_t{\mathrm{\partial }}_i$ and $D_{s}V=({\mathrm{\partial }}_s{V}^i){\mathrm{\partial }}_i+V^i{D}_s{\mathrm{\partial }}_i$. This is a local calculation, with no frame chosen over the whole rectangle.

Expand the two iterated derivatives using those coordinate formulas: the mixed ordinary derivatives of $V^i$ and the two cross terms cancel, leaving $D_s{D}_{t}V-D_t{D}_{s}V=V^i(D_s{D}_t{\mathrm{\partial }}_i-D_t{D}_s{\mathrm{\partial }}_i)$. Since $D_t{\mathrm{\partial }}_i=F_t^j{\mathrm{\nabla }}_{{\mathrm{\partial }}_j}{\mathrm{\partial }}_i$ and $D_s{\mathrm{\partial }}_i=F_s^k{\mathrm{\nabla }}_{{\mathrm{\partial }}_k}{\mathrm{\partial }}_i$, equality of the mixed partials of $F$ cancels the derivatives of $F_s,F_t$, leaving $F_s^k{F}_t^j{V}^i({\mathrm{\nabla }}_{{\mathrm{\partial }}_k}{\mathrm{\nabla }}_{{\mathrm{\partial }}_j}-{\mathrm{\nabla }}_{{\mathrm{\partial }}_j}{\mathrm{\nabla }}_{{\mathrm{\partial }}_k}){\mathrm{\partial }}_i$.

Coordinate fields commute, so $[{\mathrm{\partial }}_k,{\mathrm{\partial }}_j]=0$; by [F3] the remaining expression is $F_s^k{F}_t^j{V}^{i}R({\mathrm{\partial }}_k,{\mathrm{\partial }}_j){\mathrm{\partial }}_i$, and [F4] identifies it with $R(F_s,F_t)V$. Thus the identity holds in each local chart and on overlaps because both sides are intrinsically defined.

Smoothness to the parameter boundary extends the identity there by one-sided limits; the empty manifold has no given map $F$. If $V=0$, both sides vanish; in dimension zero every field along $F$ is zero, and in dimension one the calculation applies with curvature zero because its first two slots are alternating. Only a chart near an arbitrary point is used, so no choice principle is needed; the claim is an identity, not a biconditional. [F1, F2, F3, step 2.1] $\mathrm{\square }$