[proofplan] Each identity is verified on monomial forms $a\, dy_{i_1} \wedge \cdots \wedge dy_{i_k}$ using the $\mathbb{R}$-linearity of pullback, [exterior derivative](/theorems/1525), and wedge product. The wedge identity follows directly from the coordinate definition $F^*(a\, dy^I) = (a \circ F)\, dF^I$ together with associativity of the wedge. The exterior-derivative identity reduces to two ingredients: the chain rule, which delivers $F^*(da) = d(F^*a)$ for $0$-forms, and the [Symmetry of Second Derivatives](/theorems/332), which makes the auxiliary $2$-form $d(dF_i)$ vanish via wedge antisymmetry. Functoriality follows by computing both $(G \circ F)^*$ and $F^* \circ G^*$ on a single monomial and recognising the identity $F^*(dG_j) = d(G_j \circ F)$ produced by part (ii). [/proofplan] [step:Fix coordinates, expand in a basis, and reduce to monomial forms] Fix Cartesian coordinates $(x_1, \dots, x_m)$ on $U$ and $(y_1, \dots, y_n)$ on $V$. For an ordered multi-index $I = (i_1 < \cdots < i_k) \subseteq \{1, \dots, n\}$, write \begin{align*} dy^I &:= dy_{i_1} \wedge \cdots \wedge dy_{i_k} \in \Omega^k(V). \end{align*} Every $\omega \in \Omega^k(V)$ has a unique expansion \begin{align*} \omega &= \sum_{|I| = k} a_I\, dy^I, & a_I &\in C^\infty(V; \mathbb{R}), \end{align*} and by the [Coordinate Formula for the Pullback of a Differential Form](/theorems/3570), \begin{align*} F^*\omega &= \sum_{|I| = k} (a_I \circ F)\, dF^I, & dF^I &:= dF_{i_1} \wedge \cdots \wedge dF_{i_k}, \end{align*} where, for each $i \in \{1, \dots, n\}$, \begin{align*} dF_i &= \sum_{j=1}^m \frac{\partial F_i}{\partial x_j}\, dx_j \;\in\; \Omega^1(U). \end{align*} Because $F^*$, $d$, and $\wedge$ (in each argument) are $\mathbb{R}$-linear, it suffices to verify each identity on monomial forms $\omega = a\, dy^I$ and $\eta = b\, dy^J$ with $a, b \in C^\infty(V; \mathbb{R})$. A general $\omega$ is obtained by summation. We also record the *unordered* pullback formula \begin{align*} F^*(c\, dy_{j_1} \wedge \cdots \wedge dy_{j_s}) &= (c \circ F)\, dF_{j_1} \wedge \cdots \wedge dF_{j_s} \tag{$\ast$} \end{align*} valid for any indices $j_1, \dots, j_s \in \{1, \dots, n\}$ (not necessarily ordered, not necessarily distinct). Indeed, both sides are alternating in $(j_1, \dots, j_s)$ and agree on the strictly increasing case by the coordinate formula, so they agree on all index tuples. [/step] [step:Establish the wedge identity $F^*(\omega \wedge \eta) = F^*\omega \wedge F^*\eta$] Let $\omega = a\, dy^I$ with $|I| = k$ and $\eta = b\, dy^J$ with $|J| = \ell$. Using bilinearity of $\wedge$ over $C^\infty(V)$ — $0$-forms commute through the wedge — we compute \begin{align*} \omega \wedge \eta = (a\, dy^I) \wedge (b\, dy^J) = ab\, (dy_{i_1} \wedge \cdots \wedge dy_{i_k} \wedge dy_{j_1} \wedge \cdots \wedge dy_{j_\ell}), \end{align*} where we used [Associativity of the Wedge Product](/theorems/3559). The right-hand side is a monomial in the sense of $(\ast)$, with index tuple $(i_1, \dots, i_k, j_1, \dots, j_\ell)$. Applying $(\ast)$, \begin{align*} F^*(\omega \wedge \eta) &= (ab \circ F)\, dF_{i_1} \wedge \cdots \wedge dF_{i_k} \wedge dF_{j_1} \wedge \cdots \wedge dF_{j_\ell} \\ &= (a \circ F)(b \circ F)\, dF^I \wedge dF^J, \end{align*} again using associativity of $\wedge$ and that pointwise multiplication of $0$-forms factors as $(ab) \circ F = (a \circ F)(b \circ F)$. On the other hand, \begin{align*} F^*\omega \wedge F^*\eta &= \big[(a \circ F)\, dF^I\big] \wedge \big[(b \circ F)\, dF^J\big] = (a \circ F)(b \circ F)\, dF^I \wedge dF^J, \end{align*} since $0$-forms commute through the wedge. The two sides match. [/step] [step:Prove $F^*(da) = d(F^*a)$ for $0$-forms via the chain rule] Let $a \in C^\infty(V; \mathbb{R})$. By the [Coordinate Formula for the Exterior Derivative](/theorems/3564), \begin{align*} da &= \sum_{i=1}^n \frac{\partial a}{\partial y_i}\, dy_i \;\in\; \Omega^1(V). \end{align*} Applying $F^*$ via $(\ast)$ and the formula for $dF_i$ from Step 1, \begin{align*} F^*(da) &= \sum_{i=1}^n \!\left(\frac{\partial a}{\partial y_i} \circ F\right)\! dF_i = \sum_{j=1}^m \!\left[\,\sum_{i=1}^n \!\left(\frac{\partial a}{\partial y_i} \circ F\right)\! \frac{\partial F_i}{\partial x_j}\right]\! dx_j. \end{align*} The bracketed expression is exactly the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323) applied to the composition $a \circ F : U \to \mathbb{R}$: since $a$ and $F$ are smooth, the composite is smooth on $U$ and \begin{align*} \frac{\partial (a \circ F)}{\partial x_j}(x) &= \sum_{i=1}^n \frac{\partial a}{\partial y_i}(F(x))\, \frac{\partial F_i}{\partial x_j}(x) \quad \text{for all } x \in U. \end{align*} Substituting and invoking the [Coordinate Formula for the Exterior Derivative](/theorems/3564) once more, \begin{align*} F^*(da) &= \sum_{j=1}^m \frac{\partial (a \circ F)}{\partial x_j}\, dx_j = d(a \circ F) = d(F^*a), \end{align*} where the last equality uses that $F^*$ on $0$-forms is precomposition: $F^*a = a \circ F$. [guided] The identity $F^*(da) = d(F^*a)$ is, at its heart, just the chain rule dressed in differential-form notation. To see this, recall that $F^*$ on a $0$-form $a$ is precomposition with $F$ — there are no differentials to transform — so $F^*a = a \circ F$. The question is whether *taking $d$ before pulling back* and *pulling back before taking $d$* give the same $1$-form on $U$. Both routes can be written in coordinates. Going "$d$ first": by the [Coordinate Formula for the Exterior Derivative](/theorems/3564), \begin{align*} da &= \sum_{i=1}^n \frac{\partial a}{\partial y_i}\, dy_i. \end{align*} Now pullback. By the unordered coordinate formula $(\ast)$ from Step 1, $F^*$ acts on monomials by sending coefficients to their composites with $F$ and sending each $dy_i$ to $dF_i$, so \begin{align*} F^*(da) &= \sum_{i=1}^n \!\left(\frac{\partial a}{\partial y_i} \circ F\right)\! dF_i. \end{align*} Expand $dF_i = \sum_j (\partial F_i / \partial x_j)\, dx_j$ and collect coefficients of $dx_j$: \begin{align*} F^*(da) &= \sum_{j=1}^m \!\left[\,\sum_{i=1}^n \!\left(\frac{\partial a}{\partial y_i} \circ F\right)\! \frac{\partial F_i}{\partial x_j}\right]\! dx_j. \end{align*} Going "$F^*$ first": $F^*a = a \circ F$, so by the [Coordinate Formula for the Exterior Derivative](/theorems/3564), \begin{align*} d(F^*a) &= \sum_{j=1}^m \frac{\partial (a \circ F)}{\partial x_j}\, dx_j. \end{align*} The two routes agree if and only if, for each $j \in \{1, \dots, m\}$, \begin{align*} \frac{\partial (a \circ F)}{\partial x_j} &= \sum_{i=1}^n \!\left(\frac{\partial a}{\partial y_i} \circ F\right)\! \frac{\partial F_i}{\partial x_j}, \end{align*} which is precisely the [Chain Rule for Maps Between Euclidean Spaces](/theorems/323) for the composite $a \circ F : U \to \mathbb{R}$ in coordinates. We verify the chain rule's hypotheses: $a \in C^\infty(V; \mathbb{R})$ and $F \in C^\infty(U; V)$ are both smooth, in particular both differentiable on their domains, so the chain rule applies and the identity holds pointwise on $U$. The strategic point is that "$d$" and "$F^*$" capture different aspects of multivariable differentiation, and the chain rule is the precise statement that the two compose correctly. [/guided] [/step] [step:Show $d(dF_i) = 0$ via Symmetry of Second Derivatives] Fix $i \in \{1, \dots, n\}$ and recall $dF_i = \sum_{j=1}^m (\partial F_i / \partial x_j)\, dx_j \in \Omega^1(U)$. By the [Coordinate Formula for the Exterior Derivative](/theorems/3564) applied to the $1$-form $dF_i$, \begin{align*} d(dF_i) &= \sum_{j=1}^m d\!\left(\frac{\partial F_i}{\partial x_j}\right) \wedge dx_j = \sum_{j=1}^m \sum_{r=1}^m \frac{\partial^2 F_i}{\partial x_r\, \partial x_j}\, dx_r \wedge dx_j. \end{align*} The diagonal terms ($r = j$) carry $dx_j \wedge dx_j = 0$. For the off-diagonal terms, group the pair $\{r, j\}$ with $r < j$ and use $dx_j \wedge dx_r = -dx_r \wedge dx_j$: \begin{align*} d(dF_i) &= \sum_{1 \le r < j \le m} \!\left(\frac{\partial^2 F_i}{\partial x_r\, \partial x_j} - \frac{\partial^2 F_i}{\partial x_j\, \partial x_r}\right) dx_r \wedge dx_j. \end{align*} Since $F_i \in C^\infty(U; \mathbb{R})$, in particular $F_i$ is $C^2$ on $U$, and the [Symmetry of Second Derivatives](/theorems/332) gives \begin{align*} \frac{\partial^2 F_i}{\partial x_r\, \partial x_j}(x) &= \frac{\partial^2 F_i}{\partial x_j\, \partial x_r}(x) \quad \text{for all } x \in U. \end{align*} Every coefficient in the sum vanishes pointwise, so $d(dF_i) = 0$ as an element of $\Omega^2(U)$. [guided] The identity $d \circ d = 0$ on $0$-forms is the *one* fact behind the entire commutation of $d$ with pullback. Once we know $d(dF_i) = 0$ for the component functions $F_i$, the rest of the argument is purely algebraic — products and signs. Let us trace the structure carefully. We start with $dF_i = \sum_j (\partial F_i / \partial x_j)\, dx_j$, a $1$-form on $U$. Applying $d$ via the [Coordinate Formula for the Exterior Derivative](/theorems/3564) (each $dx_j$ is constant, so only the coefficient $\partial F_i / \partial x_j$ contributes a differential) gives \begin{align*} d(dF_i) &= \sum_{r,j=1}^m \frac{\partial^2 F_i}{\partial x_r\, \partial x_j}\, dx_r \wedge dx_j. \end{align*} The double sum has $m^2$ terms. Why does this vanish? Two facts collide: - **Analytic fact.** $\partial^2 F_i / (\partial x_r\, \partial x_j)$ is *symmetric* in $(r, j)$. This is the [Symmetry of Second Derivatives](/theorems/332), and it requires $F_i$ to be $C^2$ — which it is, since $F_i \in C^\infty(U)$. - **Algebraic fact.** $dx_r \wedge dx_j$ is *antisymmetric* in $(r, j)$: $dx_j \wedge dx_r = -dx_r \wedge dx_j$, and the diagonal $dx_j \wedge dx_j$ vanishes. When you pair a symmetric tensor against an antisymmetric one and sum over all index pairs, you get zero. Concretely, group terms by unordered pairs $\{r, j\}$ with $r \ne j$: \begin{align*} \sum_{r,j : r \ne j} \frac{\partial^2 F_i}{\partial x_r\, \partial x_j}\, dx_r \wedge dx_j &= \sum_{r < j} \!\left(\frac{\partial^2 F_i}{\partial x_r\, \partial x_j} - \frac{\partial^2 F_i}{\partial x_j\, \partial x_r}\right)\! dx_r \wedge dx_j = 0, \end{align*} the second equality being Schwarz. The diagonal $r = j$ vanishes from the wedge alone. Where would the argument fail without $C^2$ smoothness? Schwarz's theorem can fail for functions that are differentiable but not $C^2$ — counterexamples exist. The full pullback theorem genuinely requires the hypothesis that $F$ is at least $C^2$ (and we have $C^\infty$, which is more than enough). [/guided] [/step] [step:Combine Steps 2-4 to obtain $F^*(d\omega) = d(F^*\omega)$ on $k$-forms] By Step 1 it suffices to take $\omega = a\, dy^I$ with $a \in C^\infty(V; \mathbb{R})$ and $|I| = k$. By the [Coordinate Formula for the Exterior Derivative](/theorems/3564), \begin{align*} d\omega &= da \wedge dy^I. \end{align*} Applying $F^*$ and using the wedge identity from Step 2 together with the $0$-form identity from Step 3, \begin{align*} F^*(d\omega) &= F^*(da) \wedge F^*(dy^I) = d(F^*a) \wedge dF^I = d(a \circ F) \wedge dF^I. \tag{1} \end{align*} Next compute $d(F^*\omega) = d\!\big((a \circ F)\, dF^I\big)$. Expand $dF^I$ in the basis $\{dx^J\}_{|J|=k}$: by definition, \begin{align*} dF^I &= dF_{i_1} \wedge \cdots \wedge dF_{i_k} = \sum_{j_1, \dots, j_k = 1}^m \!\left(\prod_{l=1}^k \frac{\partial F_{i_l}}{\partial x_{j_l}}\right)\! dx_{j_1} \wedge \cdots \wedge dx_{j_k} =: \sum_{|J| = k} c^I_J\, dx^J, \end{align*} where each coefficient $c^I_J \in C^\infty(U; \mathbb{R})$ is the corresponding Jacobian minor. Then $F^*\omega = \sum_J (a \circ F)\, c^I_J\, dx^J$, and the [Coordinate Formula for the Exterior Derivative](/theorems/3564), combined with the product rule for $d$ on $0$-forms (which is just $d(fg) = f\, dg + g\, df$ on $0$-forms by definition of $d$ on $C^\infty(U)$), gives \begin{align*} d(F^*\omega) &= \sum_{|J|=k}\!\left[ d(a \circ F)\, c^I_J + (a \circ F)\, dc^I_J\right] \wedge dx^J \\ &= d(a \circ F) \wedge \!\left(\sum_J c^I_J\, dx^J\right) + (a \circ F) \cdot \!\left(\sum_J dc^I_J \wedge dx^J\right) \\ &= d(a \circ F) \wedge dF^I + (a \circ F) \cdot d(dF^I), \tag{2} \end{align*} where the last equality identifies $\sum_J dc^I_J \wedge dx^J$ as $d(dF^I)$ by another application of the [Coordinate Formula for the Exterior Derivative](/theorems/3564) to the $k$-form $dF^I = \sum_J c^I_J\, dx^J$. It remains to prove $d(dF^I) = 0$, after which (1) and (2) coincide and the identity is proved. **The vanishing $d(dF^I) = 0$.** From the expansion of $dF^I$ above and the [Coordinate Formula for the Exterior Derivative](/theorems/3564), \begin{align*} d(dF^I) &= \sum_{j_1, \dots, j_k} \sum_{r=1}^m \frac{\partial}{\partial x_r}\!\left(\prod_{l=1}^k \frac{\partial F_{i_l}}{\partial x_{j_l}}\right)\! dx_r \wedge dx_{j_1} \wedge \cdots \wedge dx_{j_k}. \end{align*} By the product rule for partial differentiation, \begin{align*} \frac{\partial}{\partial x_r}\!\left(\prod_{l=1}^k \frac{\partial F_{i_l}}{\partial x_{j_l}}\right) &= \sum_{s=1}^k \frac{\partial^2 F_{i_s}}{\partial x_r\, \partial x_{j_s}} \prod_{l \ne s} \frac{\partial F_{i_l}}{\partial x_{j_l}}. \end{align*} Interchanging the orders of summation, \begin{align*} d(dF^I) &= \sum_{s=1}^k \sum_{\substack{j_l : l \ne s}} \!\left(\prod_{l \ne s} \frac{\partial F_{i_l}}{\partial x_{j_l}}\right)\! \underbrace{\sum_{j_s, r = 1}^m \frac{\partial^2 F_{i_s}}{\partial x_r\, \partial x_{j_s}}\, dx_r \wedge dx_{j_1} \wedge \cdots \wedge dx_{j_k}}_{=: S_s(j_1, \dots, \widehat{j_s}, \dots, j_k)}. \end{align*} We show that $S_s = 0$ for every fixed choice of the indices $\{j_l : l \ne s\}$ and every $s$. In $S_s$ the wedge product is \begin{align*} dx_r \wedge dx_{j_1} \wedge \cdots \wedge dx_{j_k}, \end{align*} and $dx_r$ stands in the first slot while $dx_{j_s}$ stands in the $(s+1)$-th slot. Performing $s$ adjacent transpositions to move $dx_{j_s}$ next to $dx_r$ introduces a sign $(-1)^s$: \begin{align*} dx_r \wedge dx_{j_1} \wedge \cdots \wedge dx_{j_k} &= (-1)^s\, dx_r \wedge dx_{j_s} \wedge \underbrace{dx_{j_1} \wedge \cdots \widehat{dx_{j_s}} \cdots \wedge dx_{j_k}}_{\text{fixed by hypothesis}}. \end{align*} With the remaining indices held fixed, $S_s$ becomes a sum, over $(r, j_s) \in \{1, \dots, m\}^2$, of the form \begin{align*} S_s &= (-1)^s\!\sum_{r, j_s = 1}^m \frac{\partial^2 F_{i_s}}{\partial x_r\, \partial x_{j_s}}\, dx_r \wedge dx_{j_s} \wedge \omega_0, \end{align*} where $\omega_0$ is independent of $(r, j_s)$. The coefficient $\partial^2 F_{i_s} / (\partial x_r\, \partial x_{j_s})$ is symmetric in $(r, j_s)$ by the [Symmetry of Second Derivatives](/theorems/332) ($F_{i_s} \in C^\infty(U)$, in particular $C^2$), while $dx_r \wedge dx_{j_s}$ is antisymmetric in $(r, j_s)$ and vanishes on the diagonal. Exactly as in Step 4, the sum $\sum_{r, j_s} \partial^2 F_{i_s}/(\partial x_r\, \partial x_{j_s})\, dx_r \wedge dx_{j_s}$ vanishes, so $S_s = 0$ and consequently $d(dF^I) = 0$. Substituting into (2) and comparing with (1): \begin{align*} d(F^*\omega) &= d(a \circ F) \wedge dF^I + (a \circ F) \cdot 0 = d(a \circ F) \wedge dF^I = F^*(d\omega). \end{align*} [guided] The strategy is to compute both $F^*(d\omega)$ and $d(F^*\omega)$ explicitly in the $dx^J$-basis on $U$ and observe that they share the same "first-order in $a$" piece, $d(a \circ F) \wedge dF^I$, while $d(F^*\omega)$ has one additional term, $(a \circ F)\, d(dF^I)$. Everything therefore hinges on showing $d(dF^I) = 0$. Why should $d(dF^I) = 0$? Heuristically, $dF^I = dF_{i_1} \wedge \cdots \wedge dF_{i_k}$ is a wedge of exact $1$-forms, and "$d \circ d = 0$" should propagate through the wedge. The honest version of this heuristic is the Leibniz rule for $d$, which would give \begin{align*} d(dF^I) &= \sum_{l=1}^k (-1)^{l-1} dF_{i_1} \wedge \cdots \wedge d(dF_{i_l}) \wedge \cdots \wedge dF_{i_k}, \end{align*} and then each $d(dF_{i_l}) = 0$ by Step 4. Rather than invoke a Leibniz rule we have not separately proved, we **derive the same cancellation by hand** through the explicit coordinate calculation above. Let us inspect that calculation. We expand $dF^I$ in the coordinate basis $\{dx^J\}_{|J|=k}$ — a sum of terms each of the form $(\text{product of } k \text{ first-order partials of } F)\, dx_{j_1} \wedge \cdots \wedge dx_{j_k}$. Applying $d$ uses the [Coordinate Formula for the Exterior Derivative](/theorems/3564), which differentiates the coefficient and wedges it against the $dx^J$. The product rule then expresses the differentiated coefficient as a sum over which factor of the product we are differentiating — indexed by $s \in \{1, \dots, k\}$. For each fixed $s$, the contribution involves $\partial^2 F_{i_s}/(\partial x_r\, \partial x_{j_s})$ for some new index $r$ from the outer $d$, paired against the $j_s$ already in the product. This is the **same** symmetric-against-antisymmetric collision as in Step 4: the second derivative is symmetric in $(r, j_s)$ by [Symmetry of Second Derivatives](/theorems/332), and $dx_r \wedge dx_{j_s}$ is antisymmetric in $(r, j_s)$. So each $s$-contribution vanishes, and the entire $d(dF^I)$ is zero. The hypotheses we consumed: $a \in C^\infty(V; \mathbb{R})$ (so $a \circ F$ is smooth and $d(a \circ F)$ makes sense), $F \in C^\infty(U; V)$ (so all $F_i$ are at least $C^2$, enabling Schwarz; and the Jacobian minors $c^I_J$ are smooth), and the [Coordinate Formula for the Exterior Derivative](/theorems/3564) (which gives the product rule for $d$ on $0$-forms used to expand $d((a \circ F) c^I_J)$). All hypotheses are satisfied under the standing assumption $F \in C^\infty$. [/guided] [/step] [step:Establish functoriality $(G \circ F)^*\theta = F^*(G^*\theta)$] By the linearity of pullback in the form-argument it suffices to take a monomial. Let $(z_1, \dots, z_p)$ be Cartesian coordinates on $W$ and write \begin{align*} \theta &= c\, dz^K = c\, dz_{k_1} \wedge \cdots \wedge dz_{k_r}, & c &\in C^\infty(W; \mathbb{R}), \end{align*} with $K = (k_1 < \cdots < k_r) \subseteq \{1, \dots, p\}$ ordered. By the [Coordinate Formula for the Pullback of a Differential Form](/theorems/3570) applied to $G$, \begin{align*} G^*\theta &= (c \circ G)\, dG_{k_1} \wedge \cdots \wedge dG_{k_r} \;\in\; \Omega^r(V). \end{align*} Each $dG_{k_s}$ is a $1$-form on $V$. Applying $F^*$ and using identity (i) from Step 2 inductively across the $r$ factors, \begin{align*} F^*(G^*\theta) &= F^*(c \circ G) \wedge F^*(dG_{k_1}) \wedge \cdots \wedge F^*(dG_{k_r}) \\ &= \big[(c \circ G) \circ F\big] \cdot F^*(dG_{k_1}) \wedge \cdots \wedge F^*(dG_{k_r}), \tag{3} \end{align*} where $F^*$ on the $0$-form $c \circ G \in C^\infty(V; \mathbb{R})$ is precomposition: $F^*(c \circ G) = (c \circ G) \circ F$. We claim that for each $j \in \{1, \dots, p\}$, \begin{align*} F^*(dG_j) &= d(G_j \circ F). \tag{4} \end{align*} Indeed, $G_j \in C^\infty(V; \mathbb{R})$ is a $0$-form on $V$, so identity (ii) — proved in Step 5 — gives $F^*(dG_j) = d(F^*G_j) = d(G_j \circ F)$. (The hypothesis of Step 5 is satisfied: $G_j$ is a smooth $0$-form on $V$, and $F \in C^\infty(U; V)$.) Substituting (4) into (3) and using associativity of function composition $(c \circ G) \circ F = c \circ (G \circ F)$, \begin{align*} F^*(G^*\theta) &= \big[c \circ (G \circ F)\big] \cdot d(G_{k_1} \circ F) \wedge \cdots \wedge d(G_{k_r} \circ F). \tag{5} \end{align*} On the other hand, $G \circ F \in C^\infty(U; W)$ with components $(G \circ F)_j = G_j \circ F$ for each $j$. Applying the [Coordinate Formula for the Pullback of a Differential Form](/theorems/3570) directly to $G \circ F$: \begin{align*} (G \circ F)^*\theta &= \big[c \circ (G \circ F)\big] \cdot d(G \circ F)_{k_1} \wedge \cdots \wedge d(G \circ F)_{k_r} \\ &= \big[c \circ (G \circ F)\big] \cdot d(G_{k_1} \circ F) \wedge \cdots \wedge d(G_{k_r} \circ F). \tag{6} \end{align*} Expressions (5) and (6) are identical, so $F^*(G^*\theta) = (G \circ F)^*\theta$. Together with identities (i) and (ii) from Steps 2 and 5, this completes the proof of all three pullback identities. [guided] Functoriality $(G \circ F)^* = F^* \circ G^*$ is the statement that pullback reverses composition — the hallmark of a contravariant functor. The proof has a particularly clean structure once identities (i) and (ii) are established, because both sides of the identity can be computed coordinate-by-coordinate and recognised as the same expression. The key insight is what happens to the *differential factors*. On the right side, $F^*(G^*\theta)$ produces wedges of forms $F^*(dG_j)$, the pullback through $F$ of $1$-forms on $V$. On the left side, $(G \circ F)^*\theta$ produces wedges of forms $d(G_j \circ F)$, the differential on $U$ of the components of the composite. These look different, but identity (ii) — applied to the smooth $0$-form $G_j$ on $V$ — says they are equal: \begin{align*} F^*(dG_j) &= d(F^*G_j) = d(G_j \circ F). \end{align*} Once we know this, both routes produce the same expression \begin{align*} \big[c \circ (G \circ F)\big] \cdot d(G_{k_1} \circ F) \wedge \cdots \wedge d(G_{k_r} \circ F), \end{align*} and the equality is established. Notice the chain of dependencies. The identity (ii) for $0$-forms used in functoriality is exactly the chain-rule identity proved in Step 3 — *not* the full $k$-form identity from Step 5. So functoriality on monomials reduces to the chain rule, propagated through the wedge by identity (i). This explains why all three pullback identities should be regarded as a single package: (i) and (ii)-on-$0$-forms (i.e., the chain rule) are the fundamental inputs, and (ii)-on-$k$-forms and (iii) are consequences. Verifying hypotheses at each step: in invoking the [Coordinate Formula for the Pullback of a Differential Form](/theorems/3570) for the composite $G \circ F$, we need $G \circ F : U \to W$ to be smooth — and indeed the composition of smooth maps between open subsets of Euclidean spaces is smooth (the chain rule applied iteratively shows all partial derivatives of all orders exist and are continuous). The component identity $(G \circ F)_j = G_j \circ F$ is just the definition of components of a composite. [/guided] [/step]