[proofplan] The argument is the standard bundle-versus-atlas equivalence specialised to the exterior cotangent bundle. We make both objects explicit in coordinates, then build maps in both directions: a section pushes forward to a coordinate $k$-form in each chart, and the pullback formula under the transition diffeomorphism is exactly the change-of-basis law for the coordinate covectors $dx_{i_1} \wedge \cdots \wedge dx_{i_k}$. Conversely, a chart-compatible family assembles into a pointwise alternating $k$-covector field whose value at $p$ is independent of the chart precisely because of the cocycle condition. Smoothness in both directions reduces to smoothness of the coefficient functions, which is detected in any single chart. The two maps are visibly inverse on coordinate coefficients. [/proofplan] [step:Fix notation for the smooth structure on $\Lambda^k T^*M$ and write both objects in coordinates] We record the manifold and bundle structure that the proof uses. For $\alpha \in A$, write $\varphi_\alpha: U_\alpha \to \varphi_\alpha(U_\alpha) \subseteq \mathbb{R}^n$ with coordinate functions $(x_\alpha^1, \dots, x_\alpha^n)$ (here the superscripts are coordinate labels, not powers). For any pair $\alpha, \beta \in A$ with $U_{\alpha\beta} := U_\alpha \cap U_\beta \ne \varnothing$, the transition map \begin{align*} \tau_{\beta\alpha} := \varphi_\beta \circ \varphi_\alpha^{-1}: \varphi_\alpha(U_{\alpha\beta}) \to \varphi_\beta(U_{\alpha\beta}) \end{align*} is a diffeomorphism between open subsets of $\mathbb{R}^n$, and $\tau_{\alpha\beta} = \tau_{\beta\alpha}^{-1}$. For $p \in U_\alpha$ the chart gives a basis $(\partial_{x_\alpha^1}|_p, \dots, \partial_{x_\alpha^n}|_p)$ of $T_pM$ and the [dual basis](/theorems/414) $(dx_\alpha^1|_p, \dots, dx_\alpha^n|_p)$ of $T_p^*M$. For an ordered multi-index $I = (i_1 < i_2 < \cdots < i_k)$ with $1 \le i_j \le n$, set \begin{align*} dx_\alpha^I|_p := dx_\alpha^{i_1}|_p \wedge \cdots \wedge dx_\alpha^{i_k}|_p \in \Lambda^k T_p^*M. \end{align*} The collection $\{dx_\alpha^I|_p\}_{|I|=k}$ is a basis of $\Lambda^k T_p^*M$ of cardinality $\binom{n}{k}$. The smooth structure on $\Lambda^k T^*M$ is the one for which the local trivialisations \begin{align*} \Phi_\alpha: \pi^{-1}(U_\alpha) &\longrightarrow U_\alpha \times \mathbb{R}^{\binom{n}{k}} \\ \sum_{|I|=k} c_I \, dx_\alpha^I|_p &\longmapsto \bigl(p,\, (c_I)_{|I|=k}\bigr) \end{align*} are diffeomorphisms. By construction, a map $\omega: U_\alpha \to \pi^{-1}(U_\alpha)$ with $\pi \circ \omega = \mathrm{id}_{U_\alpha}$ is smooth if and only if the second component of $\Phi_\alpha \circ \omega$, i.e. the coefficient functions $c_I^\alpha: U_\alpha \to \mathbb{R}$ defined by \begin{align*} \omega(p) = \sum_{|I|=k} c_I^\alpha(p) \, dx_\alpha^I|_p, \end{align*} are smooth as functions on the manifold $U_\alpha$, which is in turn equivalent to $c_I^\alpha \circ \varphi_\alpha^{-1} \in C^\infty(\varphi_\alpha(U_\alpha))$. Finally, a chart-compatible family $\{\omega_\alpha\}_{\alpha \in A} \in \Omega^k_{\mathrm{ch}}(M, \mathcal{A})$ is, by definition, a family of smooth $k$-forms \begin{align*} \omega_\alpha = \sum_{|I|=k} f_I^\alpha \, dy^I, \qquad f_I^\alpha \in C^\infty(\varphi_\alpha(U_\alpha)), \end{align*} where $(y^1, \dots, y^n)$ are the standard coordinates on $\mathbb{R}^n$ and $dy^I = dy^{i_1} \wedge \cdots \wedge dy^{i_k}$, satisfying the cocycle compatibility from the statement. [guided] We need to commit to the basis of $\Lambda^k T^*M$ that the two definitions use, because the entire equivalence is about comparing two presentations of the same alternating tensor. Why $\binom{n}{k}$? In each tangent space $T_pM$, the exterior algebra $\Lambda^\bullet T_p^*M$ has graded dimension $\binom{n}{0}, \binom{n}{1}, \dots, \binom{n}{n}$. The $k$-th graded piece has dimension $\binom{n}{k}$, and the wedge products $dx_\alpha^{i_1} \wedge \cdots \wedge dx_\alpha^{i_k}$ with $i_1 < \cdots < i_k$ form a basis. The strict inequalities matter: any wedge with a repeated index vanishes, and we choose the increasing ordering so that the basis vectors are listed without duplication. We will index multi-indices $I = (i_1 < \cdots < i_k)$ throughout. The construction of the local trivialisations $\Phi_\alpha$ above is exactly how $\Lambda^k T^*M$ acquires its smooth manifold structure: one declares $\Phi_\alpha$ to be a diffeomorphism, and then checks that on overlaps the transition $\Phi_\beta \circ \Phi_\alpha^{-1}$ is smooth — this is precisely the smoothness of the change-of-basis matrix for the $dx^I$ between charts, which we will revisit in the next step. The takeaway is: in each chart $(U_\alpha, \varphi_\alpha)$, a section $\omega$ is captured by its coefficients $c_I^\alpha: U_\alpha \to \mathbb{R}$, and a chart-compatible local form $\omega_\alpha$ is captured by its coefficients $f_I^\alpha: \varphi_\alpha(U_\alpha) \to \mathbb{R}$. The bijection will simply be $f_I^\alpha = c_I^\alpha \circ \varphi_\alpha^{-1}$, and the entire content of the theorem is that the cocycle condition on $\{f_I^\alpha\}$ matches the well-definedness of the pointwise section $\omega(p)$. [/guided] [/step] [step:Compute the transition law for the coordinate bases $dx_\alpha^I$ and identify it with pullback under $\tau_{\beta\alpha}$] Fix $\alpha, \beta \in A$ with $U_{\alpha\beta} \ne \varnothing$ and $p \in U_{\alpha\beta}$. The two chart cobases $\{dx_\alpha^j|_p\}_{j=1}^n$ and $\{dx_\beta^j|_p\}_{j=1}^n$ of $T_p^*M$ are related by the chain rule applied to $x_\beta^j = (\tau_{\beta\alpha})^j \circ \varphi_\alpha$: \begin{align*} dx_\beta^j|_p = \sum_{\ell=1}^n \frac{\partial (\tau_{\beta\alpha})^j}{\partial y^\ell}\bigl(\varphi_\alpha(p)\bigr) \, dx_\alpha^\ell|_p, \qquad j = 1, \dots, n. \end{align*} Here we used that the entries of the differential of $\tau_{\beta\alpha}$ at $\varphi_\alpha(p)$ are exactly the partial derivatives of its component functions; the identity is the dual of the chain rule for tangent vectors. Now take wedge products. For an ordered multi-index $J = (j_1 < \cdots < j_k)$, applying the above identity to each factor and using the multilinearity and antisymmetry of $\wedge$, \begin{align*} dx_\beta^J|_p = \sum_{|I|=k} M^J_I(\varphi_\alpha(p)) \, dx_\alpha^I|_p, \end{align*} where, for ordered multi-indices $I = (i_1 < \cdots < i_k)$ and $J = (j_1 < \cdots < j_k)$, \begin{align*} M^J_I(y) := \det\!\left[\frac{\partial (\tau_{\beta\alpha})^{j_r}}{\partial y^{i_s}}(y)\right]_{r,s=1}^k \end{align*} is the $k \times k$ minor of the Jacobian matrix $J\tau_{\beta\alpha}(y)$ with row indices $J$ and column indices $I$. The matrix $M(y) = [M^J_I(y)]_{J,I}$ is the matrix of the $k$-th exterior power of the [linear map](/page/Linear%20Map) $d(\tau_{\beta\alpha})_{\varphi_\alpha(p)}$ acting on $\Lambda^k T_p^*M$, expressed in the bases $\{dx_\beta^J\}_J$ and $\{dx_\alpha^I\}_I$. Smoothness of $\tau_{\beta\alpha}$ implies $M^J_I \in C^\infty(\varphi_\alpha(U_{\alpha\beta}))$. In particular, applied to a smooth $k$-form $\eta = \sum_J g_J \, dy^J$ on $\varphi_\beta(U_{\alpha\beta})$, the [Change of Basis in Dual Space](/theorems/416) and the definition of pullback give \begin{align*} (\tau_{\beta\alpha})^* \eta = \sum_{|I|=k} \left( \sum_{|J|=k} (g_J \circ \tau_{\beta\alpha}) \cdot M^J_I \right) dy^I \end{align*} on $\varphi_\alpha(U_{\alpha\beta})$. This is the explicit local formula for the pullback used in the cocycle compatibility condition. [guided] This step is the only computation in the proof: everything else is bookkeeping. We are going to use the formula above twice — once when showing that a global section produces a compatible family, and again, read in reverse, when showing that a compatible family glues to a section. Let us double-check the chain-rule step. The smooth function $x_\beta^j: U_{\alpha\beta} \to \mathbb{R}$ decomposes as $x_\beta^j = \mathrm{pr}_j \circ \varphi_\beta = \mathrm{pr}_j \circ (\tau_{\beta\alpha} \circ \varphi_\alpha) = (\tau_{\beta\alpha})^j \circ \varphi_\alpha$. Taking its differential at $p$ and evaluating on a coordinate basis vector $\partial_{x_\alpha^\ell}|_p$, \begin{align*} dx_\beta^j|_p(\partial_{x_\alpha^\ell}|_p) = \partial_{x_\alpha^\ell}(x_\beta^j)(p) = \partial_{y^\ell}\bigl((\tau_{\beta\alpha})^j\bigr)(\varphi_\alpha(p)), \end{align*} which gives the claimed expression of $dx_\beta^j|_p$ in the $\{dx_\alpha^\ell|_p\}$ basis. The passage from $1$-form wedge products to determinant minors deserves a sanity check. For $k = 2$ and $J = (j_1, j_2)$, expanding \begin{align*} dx_\beta^{j_1} \wedge dx_\beta^{j_2} = \left( \sum_{a} A^{j_1}_a dx_\alpha^a \right) \wedge \left( \sum_b A^{j_2}_b dx_\alpha^b \right) = \sum_{a < b} (A^{j_1}_a A^{j_2}_b - A^{j_1}_b A^{j_2}_a)\, dx_\alpha^a \wedge dx_\alpha^b, \end{align*} where $A^j_\ell = \partial_{y^\ell}(\tau_{\beta\alpha})^j(\varphi_\alpha(p))$. The bracketed coefficient is the $2 \times 2$ minor $\det \begin{pmatrix} A^{j_1}_a & A^{j_1}_b \\ A^{j_2}_a & A^{j_2}_b \end{pmatrix}$, which is $M^J_I$ with $I = (a, b)$. The same calculation extends to general $k$ by induction, with each new wedge factor doubling the number of antisymmetrising terms; the result is the Leibniz expansion of the $k \times k$ determinant. Finally, the matrix-valued function $y \mapsto M^J_I(y)$ is smooth because the entries of $J\tau_{\beta\alpha}$ are smooth (composition of smooth functions: the chart transition is smooth) and the determinant is a polynomial in its entries. This is the **only** place in the proof where the differential-geometric content lives: the formula \begin{align*} (\tau_{\beta\alpha})^* \eta = \sum_{|I|=k} \left( \sum_{|J|=k} (g_J \circ \tau_{\beta\alpha}) \cdot M^J_I \right) dy^I \end{align*} will appear on both sides of the equivalence. [/guided] [/step] [step:Define the map $\Psi$ from sections to chart-compatible families] Let $\omega \in \Gamma(\Lambda^k T^*M)$. For each $\alpha \in A$, the section $\omega$ restricts to $\omega|_{U_\alpha}: U_\alpha \to \pi^{-1}(U_\alpha)$, and by the trivialisation $\Phi_\alpha$ from Step 1 there exist unique coefficient functions $c_I^\alpha: U_\alpha \to \mathbb{R}$ such that \begin{align*} \omega(p) = \sum_{|I|=k} c_I^\alpha(p)\, dx_\alpha^I|_p, \qquad p \in U_\alpha. \end{align*} By the smoothness criterion in Step 1, smoothness of $\omega$ on $U_\alpha$ is equivalent to $c_I^\alpha \in C^\infty(U_\alpha)$ for all $I$, and hence to $f_I^\alpha := c_I^\alpha \circ \varphi_\alpha^{-1} \in C^\infty(\varphi_\alpha(U_\alpha))$. Define \begin{align*} \omega_\alpha := \sum_{|I|=k} f_I^\alpha \, dy^I \in \Omega^k(\varphi_\alpha(U_\alpha)) \end{align*} and set $\Psi(\omega) := \{\omega_\alpha\}_{\alpha \in A}$. We verify the cocycle compatibility. Fix $\alpha, \beta$ with $U_{\alpha\beta} \ne \varnothing$. For $p \in U_{\alpha\beta}$, the section $\omega(p) \in \Lambda^k T_p^*M$ admits two expansions \begin{align*} \sum_{|I|=k} c_I^\alpha(p)\, dx_\alpha^I|_p = \omega(p) = \sum_{|J|=k} c_J^\beta(p)\, dx_\beta^J|_p, \end{align*} and substituting the basis-change relation from Step 2 into the right-hand side and matching coefficients of $dx_\alpha^I|_p$ gives \begin{align*} c_I^\alpha(p) = \sum_{|J|=k} c_J^\beta(p) \, M^J_I(\varphi_\alpha(p)). \end{align*} Composing with $\varphi_\alpha^{-1}$ and using $c_J^\beta \circ \varphi_\alpha^{-1} = f_J^\beta \circ \tau_{\beta\alpha}$ on $\varphi_\alpha(U_{\alpha\beta})$, \begin{align*} f_I^\alpha = \sum_{|J|=k} (f_J^\beta \circ \tau_{\beta\alpha}) \cdot M^J_I \qquad \text{on } \varphi_\alpha(U_{\alpha\beta}). \end{align*} By the explicit pullback formula derived at the end of Step 2 (applied with $\eta = \omega_\beta$, hence $g_J = f_J^\beta$), this is exactly $\omega_\alpha = (\tau_{\beta\alpha})^* \omega_\beta$ on $\varphi_\alpha(U_{\alpha\beta})$, which is the required cocycle compatibility. Hence $\Psi(\omega) \in \Omega^k_{\mathrm{ch}}(M, \mathcal{A})$. [guided] The construction is purely tautological once Step 2 is in place: the section $\omega$ already takes values in the exterior cotangent bundle, so at each point and in each chart its value can be unambiguously written in the basis $\{dx_\alpha^I|_p\}$. The coefficients $c_I^\alpha(p)$ are nothing other than the components of $\omega(p)$ with respect to that basis. Why do we need to verify the cocycle condition? Because the two chart presentations $\omega_\alpha$ and $\omega_\beta$ live on different open subsets of $\mathbb{R}^n$, and the only information that ties them together is that they came from a single global object $\omega$. The condition $\omega_\alpha = (\tau_{\beta\alpha})^* \omega_\beta$ on overlaps is the abstract way of saying "both presentations agree pointwise on $U_{\alpha\beta}$ after the appropriate coordinate change." The calculation works as follows. The value $\omega(p) \in \Lambda^k T_p^*M$ is intrinsic; choosing two coordinate bases gives two coordinate presentations. Equating them and substituting the basis-change matrix $M$ from Step 2 produces a system of equalities for the coordinate coefficients. These equalities, transported to $\mathbb{R}^n$ via the chart maps, are exactly the local-coordinate formula for the pullback that we computed in Step 2. This is the formula \begin{align*} f_I^\alpha(y) = \sum_{|J|=k} f_J^\beta(\tau_{\beta\alpha}(y)) \cdot M^J_I(y), \qquad y \in \varphi_\alpha(U_{\alpha\beta}), \end{align*} which we recognise as the chartwise expansion of $(\tau_{\beta\alpha})^* \omega_\beta$. Hence $\omega_\alpha = (\tau_{\beta\alpha})^* \omega_\beta$, the cocycle is satisfied, and $\Psi$ produces a valid chart-compatible family. Smoothness of the $f_I^\alpha$ is automatic from smoothness of the section $\omega$, via the smoothness criterion in the local trivialisation $\Phi_\alpha$. We have not used any deep results — only the chain rule and the definition of the smooth structure on $\Lambda^k T^*M$. [/guided] [/step] [step:Define the inverse map $\Psi^{-1}$ from chart-compatible families to sections] Let $\{\omega_\alpha\}_{\alpha \in A} \in \Omega^k_{\mathrm{ch}}(M, \mathcal{A})$ with $\omega_\alpha = \sum_I f_I^\alpha \, dy^I$ and $f_I^\alpha \in C^\infty(\varphi_\alpha(U_\alpha))$. For each $p \in M$ pick any $\alpha \in A$ with $p \in U_\alpha$ and set \begin{align*} \omega(p) := \sum_{|I|=k} f_I^\alpha(\varphi_\alpha(p))\, dx_\alpha^I|_p \;\in\; \Lambda^k T_p^*M. \end{align*} We claim $\omega(p)$ does not depend on the choice of chart $\alpha$ containing $p$. Suppose $p \in U_\alpha \cap U_\beta$. The cocycle condition reads $\omega_\alpha = (\tau_{\beta\alpha})^* \omega_\beta$ on $\varphi_\alpha(U_{\alpha\beta})$, which by the local pullback formula from Step 2 is \begin{align*} f_I^\alpha(y) = \sum_{|J|=k} f_J^\beta(\tau_{\beta\alpha}(y)) \cdot M^J_I(y), \qquad y \in \varphi_\alpha(U_{\alpha\beta}). \end{align*} Evaluating at $y = \varphi_\alpha(p)$ (so $\tau_{\beta\alpha}(y) = \varphi_\beta(p)$) and multiplying by $dx_\alpha^I|_p$, then summing over $I$ and applying the basis-change identity $\sum_I M^J_I(\varphi_\alpha(p))\, dx_\alpha^I|_p = dx_\beta^J|_p$ from Step 2, \begin{align*} \sum_{|I|=k} f_I^\alpha(\varphi_\alpha(p))\, dx_\alpha^I|_p \;=\; \sum_{|J|=k} f_J^\beta(\varphi_\beta(p))\, dx_\beta^J|_p. \end{align*} Hence the definition of $\omega(p)$ is independent of $\alpha$. By construction $\omega: M \to \Lambda^k T^*M$ satisfies $\pi \circ \omega = \mathrm{id}_M$. It remains to verify smoothness. By the smoothness criterion in Step 1, $\omega|_{U_\alpha}$ is smooth as a section if and only if the coefficient functions $p \mapsto f_I^\alpha(\varphi_\alpha(p))$ are smooth as functions $U_\alpha \to \mathbb{R}$. These are compositions of the smooth chart map $\varphi_\alpha: U_\alpha \to \varphi_\alpha(U_\alpha)$ with the smooth function $f_I^\alpha: \varphi_\alpha(U_\alpha) \to \mathbb{R}$, hence smooth. Since smoothness is a local property and $\{U_\alpha\}_{\alpha \in A}$ covers $M$, $\omega$ is a smooth section. Define $\Psi^{-1}(\{\omega_\alpha\}) := \omega$. [guided] This is the reverse construction: we are given chartwise data and must glue it into a global geometric object. The recipe is mechanical: at each point $p$, pick any chart $\alpha$ containing $p$, read off the coefficients $f_I^\alpha(\varphi_\alpha(p))$, and assemble the alternating $k$-covector $\sum_I f_I^\alpha(\varphi_\alpha(p)) \, dx_\alpha^I|_p$ in $\Lambda^k T_p^*M$. The question is whether this is consistent: if $p$ lies in two charts, do we get the same alternating $k$-covector from each chart? This is exactly what the cocycle condition $\omega_\alpha = (\tau_{\beta\alpha})^* \omega_\beta$ guarantees. The cocycle condition is, by the local pullback formula from Step 2, an equality of coefficient functions on overlaps: \begin{align*} f_I^\alpha(y) = \sum_{|J|=k} f_J^\beta(\tau_{\beta\alpha}(y)) \cdot M^J_I(y). \end{align*} Plug $y = \varphi_\alpha(p)$; note that $\tau_{\beta\alpha}(\varphi_\alpha(p)) = \varphi_\beta(p)$ by definition of the transition. The right-hand side becomes a linear combination of $f_J^\beta(\varphi_\beta(p))$, whose vector of coefficients $(M^J_I(\varphi_\alpha(p)))_{I}$ is exactly the basis-change vector expressing $dx_\beta^J|_p$ in the $\{dx_\alpha^I|_p\}$ basis. Pairing both sides with $dx_\alpha^I|_p$ and summing collapses the basis change, leaving the same intrinsic $k$-covector $\omega(p)$ regardless of chart. The smoothness verification is automatic: $f_I^\alpha$ is smooth on $\varphi_\alpha(U_\alpha) \subset \mathbb{R}^n$ by hypothesis; precomposing with the smooth chart $\varphi_\alpha$ gives a smooth function on $U_\alpha$. By the local-trivialisation smoothness criterion from Step 1, the corresponding section is smooth on $U_\alpha$. Smoothness is local, so $\omega$ is smooth on all of $M$. Notice what would go wrong if we did not have the cocycle condition: pointwise values would depend on the chart, so $\omega(p)$ would not even be a well-defined map $M \to \Lambda^k T^*M$, let alone a section. [/guided] [/step] [step:Verify $\Psi$ and $\Psi^{-1}$ are mutually inverse] Let $\omega \in \Gamma(\Lambda^k T^*M)$, and let $\Psi(\omega) = \{\omega_\alpha\}$ with $\omega_\alpha = \sum_I f_I^\alpha \, dy^I$ and $f_I^\alpha = c_I^\alpha \circ \varphi_\alpha^{-1}$. Then by the definition of $\Psi^{-1}$ in Step 4, for any $p \in U_\alpha$, \begin{align*} (\Psi^{-1} \circ \Psi)(\omega)(p) = \sum_{|I|=k} f_I^\alpha(\varphi_\alpha(p))\, dx_\alpha^I|_p = \sum_{|I|=k} c_I^\alpha(p)\, dx_\alpha^I|_p = \omega(p), \end{align*} by the definition of $c_I^\alpha$ in Step 3. Hence $\Psi^{-1} \circ \Psi = \mathrm{id}_{\Gamma(\Lambda^k T^*M)}$. Conversely, let $\{\omega_\alpha\} \in \Omega^k_{\mathrm{ch}}(M, \mathcal{A})$ with $\omega_\alpha = \sum_I f_I^\alpha \, dy^I$, set $\omega := \Psi^{-1}(\{\omega_\alpha\})$, and let $\Psi(\omega) = \{\omega_\alpha'\}_{\alpha \in A}$. By Step 3, $\omega_\alpha' = \sum_I (c_I^\alpha \circ \varphi_\alpha^{-1}) \, dy^I$, where $c_I^\alpha$ are the coefficients of $\omega$ in the basis $\{dx_\alpha^I\}$. By construction of $\omega$ in Step 4, $c_I^\alpha(p) = f_I^\alpha(\varphi_\alpha(p))$, so $c_I^\alpha \circ \varphi_\alpha^{-1} = f_I^\alpha$ on $\varphi_\alpha(U_\alpha)$. Hence $\omega_\alpha' = \omega_\alpha$ for every $\alpha$, i.e. $\Psi \circ \Psi^{-1} = \mathrm{id}_{\Omega^k_{\mathrm{ch}}(M, \mathcal{A})}$. This establishes the bijection. Finally, both $\Psi$ and $\Psi^{-1}$ are $\mathbb{R}$-linear by inspection of the coefficient formulas, and they commute with multiplication by $h \in C^\infty(M)$ since multiplication acts on coefficient functions chartwise as $c_I^\alpha \mapsto h \cdot c_I^\alpha$ on the section side and as $f_I^\alpha \mapsto (h \circ \varphi_\alpha^{-1}) \cdot f_I^\alpha$ on the chart side, and these are compatible under $f_I^\alpha = c_I^\alpha \circ \varphi_\alpha^{-1}$. Hence $\Psi$ is a $C^\infty(M)$-module isomorphism, completing the proof. [guided] This step is the formal verification that what we wrote down is actually a bijection. The two compositions are checked by tracing the coefficient functions through both constructions and noticing that everything collapses to the identity. In the direction $\Psi^{-1} \circ \Psi$: starting with a section $\omega$, $\Psi$ records its coefficients $c_I^\alpha$ in each chart and transports them to functions $f_I^\alpha = c_I^\alpha \circ \varphi_\alpha^{-1}$ on $\mathbb{R}^n$. Then $\Psi^{-1}$ evaluates $f_I^\alpha$ at $\varphi_\alpha(p)$ — undoing the transport — to recover $c_I^\alpha(p)$, which by definition rebuilds $\omega(p)$. In the direction $\Psi \circ \Psi^{-1}$: starting with a chart family $\{\omega_\alpha\}$, $\Psi^{-1}$ defines a section whose coefficient at $p$ in chart $\alpha$ is precisely $f_I^\alpha(\varphi_\alpha(p))$. Then $\Psi$ reads off those coefficients and transports them back to $\mathbb{R}^n$, recovering $f_I^\alpha$ identically. The module structure compatibility is similarly tautological: scalar multiplication and addition act linearly on coefficients in any basis, and the bijection $\Psi$ is defined purely by reading off coefficients. There is nothing more to verify. We have therefore established that the two definitions of "smooth $k$-form on $M$" — as a chart-compatible family of local coordinate forms, or as a smooth section of the bundle $\Lambda^k T^*M$ — describe exactly the same mathematical objects, with the equivalence given by the canonical map $\Psi$ which is, in every chart, the identity on coefficient functions transported through $\varphi_\alpha$. [/guided] [/step]