[proofplan] The argument reduces the global statement to a pointwise linear-algebra fact and a smoothness verification. At each $x \in U$ the cotangent space $T_x^*U$ is canonically $(\mathbb{R}^n)^*$ with basis $dx_1|_x, \dots, dx_n|_x$, so by the basis theorem for exterior powers the increasing wedge products form a basis of $\Lambda^k(T_x^*U)$; this forces the coefficients of $\omega_x$ to be uniquely determined pointwise. We then identify these pointwise coefficients via the duality pairing $a_I(x) = \omega_x(\partial_{x_{i_1}}|_x, \dots, \partial_{x_{i_k}}|_x)$ and use the definition of smoothness of a differential form (smoothness against smooth vector field inputs) to conclude $a_I \in C^\infty(U)$. The reverse direction — that any choice of smooth coefficients defines a smooth form — together with the fact that addition and scaling of differential forms act coefficientwise establishes the free module structure. [/proofplan]

[step:Set up the pointwise framework on $T_x^*U$]For each $x \in U$ identify $T_xU$ with $\mathbb{R}^n$ via the standard chart, so that the coordinate tangent vectors \begin{align*} \partial_{x_1}|_x, \dots, \partial_{x_n}|_x \in T_xU \end{align*} form a basis of $T_xU$, and the coordinate covectors \begin{align*} dx_1|_x, \dots, dx_n|_x \in T_x^*U \end{align*} form the [dual basis](/theorems/414), characterised by $dx_i|_x(\partial_{x_j}|_x) = \delta_{ij}$ for $1 \le i, j \le n$. Recall that a differential $k$-form on $U$ is, by definition, a section \begin{align*} \omega : U &\to \Lambda^k T^*U \\ x &\mapsto \omega_x \in \Lambda^k(T_x^*U) \end{align*} which is smooth in the sense that for every $k$-tuple of smooth vector fields $X_1, \dots, X_k \in \mathfrak{X}(U)$, the scalar function \begin{align*} \omega(X_1, \dots, X_k) : U &\to \mathbb{R} \\ x &\mapsto \omega_x(X_1(x), \dots, X_k(x)) \end{align*} belongs to $C^\infty(U)$.[/step]

[guided]Before extracting coefficients we fix the precise framework. The chart structure of $U \subseteq \mathbb{R}^n$ gives a canonical identification of every tangent space with $\mathbb{R}^n$: the vectors $\partial_{x_1}|_x, \dots, \partial_{x_n}|_x \in T_xU$ are the standard coordinate basis, and dually $dx_1|_x, \dots, dx_n|_x \in T_x^*U$ are characterised by the duality relation \begin{align*} dx_i|_x(\partial_{x_j}|_x) = \delta_{ij}, \quad 1 \le i, j \le n. \end{align*} It is crucial to state which definition of "smooth differential form" we use, because the entire theorem amounts to passing between the bundle-theoretic and the coefficientwise descriptions of smoothness. We adopt the following: a section $\omega$ of $\Lambda^k T^*U \to U$ is **smooth** iff for every choice of smooth vector fields $X_1, \dots, X_k \in \mathfrak{X}(U)$, the function $x \mapsto \omega_x(X_1(x), \dots, X_k(x))$ is smooth on $U$. This definition is the operative one in what follows; the equivalence with other definitions (smoothness as a section in the bundle sense, smoothness of coefficients in any chart) is part of what we are proving.[/guided]

[step:Apply the exterior-power basis theorem pointwise]Fix $x \in U$. By the [Dimensions of Symmetric and Exterior Powers](/theorems/3303), applied to the $n$-dimensional [vector space](/page/Vector%20Space) $T_x^*U$ with basis $\{dx_1|_x, \dots, dx_n|_x\}$, the family \begin{align*} \mathcal{B}_k(x) := \bigl\{ dx_{i_1}|_x \wedge \dots \wedge dx_{i_k}|_x : 1 \le i_1 < \dots < i_k \le n \bigr\} \end{align*} is a basis of $\Lambda^k(T_x^*U)$, which has dimension $\binom{n}{k}$. Consequently there exist unique scalars $a_I(x) \in \mathbb{R}$, indexed by strictly increasing multi-indices $I = (i_1, \dots, i_k)$, such that \begin{align*} \omega_x = \sum_{1 \le i_1 < \dots < i_k \le n} a_{i_1 \dots i_k}(x)\, dx_{i_1}|_x \wedge \dots \wedge dx_{i_k}|_x. \tag{$\ast$} \end{align*} Letting $x$ vary, this defines functions $a_I : U \to \mathbb{R}$ for each increasing multi-index $I$.[/step]

[guided]The pointwise expansion is forced by linear algebra, not differential geometry: at the fixed point $x$, the cotangent space $T_x^*U$ is just an $n$-dimensional real [vector space](/page/Vector%20Space) with a distinguished basis, and theorem 3303 supplies the basis of its $k$-th exterior power. The hypotheses of theorem 3303 require a [vector space](/page/Vector%20Space) over a field of characteristic zero (or at least one where $k!$ is invertible); we are over $\mathbb{R}$, so this holds vacuously. Why use strictly **increasing** multi-indices? Because the wedge product is alternating: $dx_i \wedge dx_j = -dx_j \wedge dx_i$ and $dx_i \wedge dx_i = 0$. Any wedge $dx_{j_1} \wedge \dots \wedge dx_{j_k}$ with a repeated index vanishes, and any wedge with distinct indices equals $\pm$ the wedge in increasing order. Restricting to increasing multi-indices removes both the sign ambiguity and the redundancy, yielding a basis (not just a spanning set) of size $\binom{n}{k}$. The uniqueness of the scalars $a_I(x)$ at each $x$ is precisely the [linear independence](/page/Linear%20Independence) of $\mathcal{B}_k(x)$. Varying $x$ produces well-defined functions $a_I : U \to \mathbb{R}$. The remaining task is to verify that these functions are smooth on $U$ — pointwise uniqueness does not yet give smoothness.[/guided]

[step:Identify the coefficients via the duality pairing]We claim that the coefficient $a_I$ in $(\ast)$ is given by \begin{align*} a_I(x) = \omega_x\bigl(\partial_{x_{i_1}}|_x, \dots, \partial_{x_{i_k}}|_x\bigr), \quad x \in U, \end{align*} for each increasing multi-index $I = (i_1, \dots, i_k)$. To prove this, recall that for covectors $\alpha_1, \dots, \alpha_k \in T_x^*U$ and tangent vectors $v_1, \dots, v_k \in T_xU$, the wedge product evaluates as \begin{align*} (\alpha_1 \wedge \dots \wedge \alpha_k)(v_1, \dots, v_k) = \det\bigl( \alpha_p(v_q) \bigr)_{p,q=1}^k. \end{align*} Apply this to $\alpha_p = dx_{j_p}|_x$ and $v_q = \partial_{x_{i_q}}|_x$ for increasing multi-indices $J = (j_1, \dots, j_k)$ and $I = (i_1, \dots, i_k)$. Using $dx_{j_p}|_x(\partial_{x_{i_q}}|_x) = \delta_{j_p, i_q}$: \begin{align*} \bigl( dx_{j_1} \wedge \dots \wedge dx_{j_k} \bigr)\bigl( \partial_{x_{i_1}}, \dots, \partial_{x_{i_k}} \bigr)\Big|_x = \det\bigl( \delta_{j_p, i_q} \bigr)_{p,q=1}^k = \delta_{IJ}, \end{align*} where $\delta_{IJ} = 1$ if $I = J$ and $0$ otherwise. Indeed, if $I \ne J$ then either some $j_p$ does not appear among the $i_q$ (giving a zero row) or some $i_q$ does not appear among the $j_p$ (giving a zero column); if $I = J$ then since both multi-indices are strictly increasing, $j_p = i_p$ for all $p$ and the matrix is the identity. Evaluating both sides of $(\ast)$ on the tuple $(\partial_{x_{i_1}}|_x, \dots, \partial_{x_{i_k}}|_x)$ gives \begin{align*} \omega_x(\partial_{x_{i_1}}|_x, \dots, \partial_{x_{i_k}}|_x) = \sum_J a_J(x)\, \delta_{IJ} = a_I(x), \end{align*} as claimed.[/step]

[guided]The strategy is dual: the basis $\mathcal{B}_k(x)$ of $\Lambda^k(T_x^*U)$ has a [dual basis](/theorems/414) in $\Lambda^k(T_xU) \cong (\Lambda^k T_x^*U)^*$, namely the increasing wedges $\partial_{x_{i_1}}|_x \wedge \dots \wedge \partial_{x_{i_k}}|_x$, and pairing $\omega_x$ with these [dual basis](/theorems/414) elements extracts the coefficients $a_I(x)$. Concretely: evaluating a wedge of covectors on a tuple of vectors is the determinant formula \begin{align*} (\alpha_1 \wedge \dots \wedge \alpha_k)(v_1, \dots, v_k) = \det\bigl(\alpha_p(v_q)\bigr)_{p, q = 1}^k, \end{align*} which is the defining property of $\wedge$ as the alternation of the [tensor product](/page/Tensor%20Product). We evaluate the basis wedge $dx_{j_1} \wedge \dots \wedge dx_{j_k}$ on the tuple $(\partial_{x_{i_1}}, \dots, \partial_{x_{i_k}})$ at $x$ to obtain \begin{align*} \det\bigl(\delta_{j_p, i_q}\bigr)_{p, q = 1}^k. \end{align*} Why does this determinant equal $\delta_{IJ}$ when $I$ and $J$ are both strictly increasing? If the multi-indices differ, say there is some $j_p$ not in $\{i_1, \dots, i_k\}$, then the entire $p$-th row of the matrix is zero, killing the determinant. Symmetrically a missing $i_q$ kills the $q$-th column. If $I = J$, then because both are strictly increasing the only way to match $j_p$ to $i_q$ is $p = q$, so the matrix is the $k \times k$ identity and the determinant is $1$. (If we did not require increasing order, we would pick up sign permutations; the increasing convention is what makes the [dual basis](/theorems/414) pairing diagonal.) Plugging the tuple $(\partial_{x_{i_1}}|_x, \dots, \partial_{x_{i_k}}|_x)$ into the expansion $(\ast)$ collapses the sum to the single term $a_I(x)$.[/guided]

[step:Deduce smoothness of the coefficients]For each increasing multi-index $I = (i_1, \dots, i_k)$, the coordinate vector fields \begin{align*} \partial_{x_{i_1}}, \dots, \partial_{x_{i_k}} \in \mathfrak{X}(U) \end{align*} are smooth (each is the constant section of $TU \cong U \times \mathbb{R}^n$ equal to the $i_p$-th standard basis vector). By the smoothness hypothesis on $\omega$ (Step 1), the function \begin{align*} x \mapsto \omega_x(\partial_{x_{i_1}}|_x, \dots, \partial_{x_{i_k}}|_x) = a_I(x) \end{align*} belongs to $C^\infty(U)$. Therefore $a_I \in C^\infty(U)$ for every increasing multi-index $I$. This establishes both existence and uniqueness of the smooth coefficient expansion: existence follows from $(\ast)$ together with smoothness just proved, and uniqueness is the uniqueness already obtained pointwise in Step 2 (if two smooth expansions agreed pointwise on $U$, then at each $x$ their coefficients would agree by the pointwise [linear independence](/page/Linear%20Independence) of $\mathcal{B}_k(x)$).[/step]

[guided]The smoothness of each $a_I$ is now an immediate consequence of the definition of "smooth differential form" stated in Step 1. The standard coordinate vector fields $\partial_{x_i}$ are smooth on $U$ because under the trivialisation $TU \cong U \times \mathbb{R}^n$ they correspond to the constant sections $x \mapsto (x, e_i)$, which are visibly smooth. Plugging the $k$-tuple $(\partial_{x_{i_1}}, \dots, \partial_{x_{i_k}})$ into the smoothness hypothesis for $\omega$ yields exactly the function $a_I$ from Step 3, and the hypothesis guarantees this function is smooth. Notice what we have shown: **smoothness of a differential form (as a section) is equivalent to smoothness of its coefficients in the coordinate basis**. Half of the equivalence is the present step (section smoothness implies coefficient smoothness); the converse is Step 5 below. Uniqueness of the smooth expansion is automatic from the pointwise uniqueness of Step 2: if $\sum_I a_I\, dx_I = \sum_I b_I\, dx_I$ everywhere on $U$, then at each $x$ the family $\mathcal{B}_k(x)$ is linearly independent so $a_I(x) = b_I(x)$ for all $I$, i.e. $a_I = b_I$ as functions on $U$.[/guided]

[step:Conclude the free $C^\infty(U)$-module structure]The $C^\infty(U)$-module structure on $\Omega^k(U)$ is defined pointwise: \begin{align*} (\omega + \eta)_x &:= \omega_x + \eta_x, \\ (f \cdot \omega)_x &:= f(x)\, \omega_x, \end{align*} for $\omega, \eta \in \Omega^k(U)$, $f \in C^\infty(U)$, $x \in U$. (The right-hand sides are smooth sections because the operations are smooth pointwise and the smoothness of the inputs implies the smoothness of the output: if $\omega, \eta$ are smooth then $(\omega+\eta)(X_1, \dots, X_k) = \omega(X_1, \dots, X_k) + \eta(X_1, \dots, X_k) \in C^\infty(U)$, and similarly for $f\cdot \omega$.) Under the pointwise expansion of Steps 2–4, these operations act coefficientwise: if \begin{align*} \omega = \sum_I a_I\, dx_{i_1} \wedge \dots \wedge dx_{i_k}, \qquad \eta = \sum_I b_I\, dx_{i_1} \wedge \dots \wedge dx_{i_k}, \end{align*} then \begin{align*} \omega + \eta &= \sum_I (a_I + b_I)\, dx_{i_1} \wedge \dots \wedge dx_{i_k}, \\ f \cdot \omega &= \sum_I (f \cdot a_I)\, dx_{i_1} \wedge \dots \wedge dx_{i_k}. \end{align*} This is the assertion that the map \begin{align*} \Phi : \Omega^k(U) &\to C^\infty(U)^{\binom{n}{k}} \\ \omega &\mapsto (a_I)_I \end{align*} is a $C^\infty(U)$-module homomorphism. By Steps 2–4 the map $\Phi$ is bijective: surjectivity is the observation that for any choice of smooth $a_I \in C^\infty(U)$ the section $\sum_I a_I\, dx_{i_1} \wedge \dots \wedge dx_{i_k}$ is a smooth $k$-form (its evaluation on any smooth tuple of vector fields is a polynomial in the $a_I$ and the components of those vector fields, hence smooth), and injectivity is the uniqueness from Step 4. Hence $\Phi$ is a $C^\infty(U)$-module isomorphism, and \begin{align*} \Omega^k(U) \cong C^\infty(U)^{\binom{n}{k}} \end{align*} as a free $C^\infty(U)$-module with basis $\mathcal{B}_k = \{dx_{i_1} \wedge \dots \wedge dx_{i_k} : 1 \le i_1 < \dots < i_k \le n\}$.[/step]

[guided]The final step packages the coefficientwise correspondence as a module isomorphism. The pointwise [vector space](/page/Vector%20Space) operations on $\Lambda^k(T_x^*U)$ assemble to module operations on $\Omega^k(U)$ over the ring $C^\infty(U)$ — multiplication by a scalar function $f \in C^\infty(U)$ rescales $\omega_x$ by $f(x)$ at each point. These operations are visibly coefficientwise in the basis $\mathcal{B}_k$, so the assignment \begin{align*} \Phi : \omega \mapsto (a_I)_I \end{align*} is a $C^\infty(U)$-[linear map](/page/Linear%20Map) into $C^\infty(U)^{\binom{n}{k}}$. Injectivity of $\Phi$ is the uniqueness already proved. Surjectivity requires checking that given an arbitrary $\binom{n}{k}$-tuple of smooth functions $a_I \in C^\infty(U)$, the section \begin{align*} \omega = \sum_I a_I\, dx_{i_1} \wedge \dots \wedge dx_{i_k} \end{align*} really is a smooth differential form. We check this using the definition of smoothness from Step 1: for smooth vector fields $X_1, \dots, X_k \in \mathfrak{X}(U)$, write $X_q = \sum_{j} X_{q,j}\, \partial_{x_j}$ with $X_{q,j} \in C^\infty(U)$. Then \begin{align*} \omega(X_1, \dots, X_k) = \sum_I a_I\, \det(X_{q, i_p})_{p, q = 1}^k, \end{align*} which is a finite sum of products of smooth functions and is therefore smooth. So $\Phi$ is surjective, and we conclude $\Phi$ is a $C^\infty(U)$-module isomorphism $\Omega^k(U) \cong C^\infty(U)^{\binom{n}{k}}$. This exhibits $\Omega^k(U)$ as a free $C^\infty(U)$-module of rank $\binom{n}{k}$ with basis $\mathcal{B}_k$, completing the proof.[/guided]