Induced connections commute with contraction and permutation

For an elementary tensor, applying a permutation to the sum of derivatives in [F1] merely moves each differentiated slot to its permuted position. Differentiating the permuted tensor gives exactly this reordered sum, with no sign for ordinary tensor permutation. Thus the first identity holds on elementary tensors.

For a tensor with contracted factors $\alpha ,s$ and remaining tensor $T$, contraction yields $\alpha (s)T$. Its derivative is $X(\alpha (s))T+\alpha (s){\mathrm{\nabla }}_{X}T$. The two terms from differentiating the contracted factors before contraction are $(({\mathrm{\nabla }}_X\alpha )(s)+\alpha ({\mathrm{\nabla }}_{X}s))T=X(\alpha (s))T$ by duality. The remaining differentiated slots give $\alpha (s){\mathrm{\nabla }}_{X}T$. This proves the contraction identity on elementary tensors, including full contraction where $T=1$.

Expand a general local section in finitely many product-frame tensors. Both sides of either identity add the same coefficient-derivative term $X(f)$ on a term $fT$, so the established identities extend to every section. Identity permutations, zero tensors and zero-rank factors are included. With no tensor slots the connection is scalar differentiation and the empty permutation is the identity; contractions require an actual dual/primal pair. The argument is local and uses no AC.