The de Rham complex and pullback extend to manifolds with boundary

Near a fixed boundary-chart point there are finitely many coefficients in a form. Intersect their finitely many extension neighbourhoods and apply [F3] to these extensions on that open set. By [F2], replacing any extension leaves each first derivative on the half-space unchanged. Thus the resulting restricted $(k+1)$-form is well defined and has locally extendible coefficients. The construction is local at each point and selects no extensions over a family of chart points.

On a chart overlap let $g$ be the transition map. Locally extend its coordinate functions and the finitely many target coefficients, shrinking the source extension neighbourhood so that its image lies in the open set of coefficient extensions; continuity at the specified point ensures this. The coordinate identity for the original form is the equality of its source coefficients with those of $g^{\ast }$ of its target coefficients on the half-space. By [F2] their derivatives agree there. Applying [F4] to the Euclidean extensions yields $d(g^{\ast }\eta )=g^{\ast }(d\eta )$ on the half-space. Therefore the local derivatives in step 1.1 obey the form transformation rule and patch to a single form on $M$. This uses local extensions, not a demand that an extended transition map remain inside the half-space.

To compute $d^2$, use the first derivatives of the same coefficient extensions to represent the first derivative form, which is permitted by step 1.1. Equation [F5] then restricts to $d^2=0$ on the half-space. Likewise [F6], applied to simultaneous local extensions of two forms and restricted back, proves real linearity and the signed product rule. All these identities patch by step 2.1. This calculation explicitly includes the vanishing of $d^2$ of each function that occurs when differentiating a wedge of pulled-back coordinate differentials.

At a specified point of $M$, [F9] extends the coordinate representative of $F$ to a Euclidean-open set. Extend a target form's finitely many coefficients near its image and shrink the source as in step 2.1. The Euclidean pullback, derivative and wedge identities of [F4] and [F7] restrict to the corresponding identities on $M$, independently of all extensions by [F2]. This works even if $F$ maps an open set entirely into $\mathrm{\partial }N$: the Euclidean calculation takes place before restriction and does not presume that $F$ carries interior points to interior points. Composition and identity laws follow from the same local formulas.

Step 3.1 puts $\mathrm{im}d\subseteq \ker d$, so the stated vector-space quotient is defined. By step 3.2, a closed form pulls back to a closed form, and a change by $d\eta$ pulls back to a change by $d(F^{\ast }\eta )$; hence the quotient maps are well defined and functorial. On boundaryless charts the construction is exactly [F8]. For dimension zero, all positive-degree forms vanish and $d=0$; the empty manifold has only zero section spaces. At boundary points step 1.1 handles every derivative by [F2], and no orientation or nonempty choice is required.