A normalized compactly supported top form on Euclidean space

Take $\rho$ from [F1] and set $a={\int }_{-1}^1\rho (t)dt$. The partition at $-1\mathrm{/}2$ and $1\mathrm{/}2$, together with $\rho \ge 0$ everywhere and $\rho =1$ on the central interval, has lower Darboux sum at least $1$; hence [F2] gives $a\ge 1>0$. Put $b=\rho \mathrm{/}a$. Then $b$ is smooth, supported in $(-1,1)$, and ${\int }_{\mathbb{R}}b=1$.

Using the library's zero-based coordinates on $n=\{0,\dots ,n-1\}$, define $\omega (x_0,\dots ,x_{n-1})=({\prod }_{j=0}^{n-1}b(x_j))d{x}^0\wedge \cdots \wedge d{x}^{n-1}\mathrm{.}$ Its coefficient is smooth and its support lies in the closed cube $[-1,1{]}^n$, which is compact by [F3]. Repeated application of [F3] on that cube gives ${\int }_{{\mathbb{R}}^n}\omega ={\prod }_{j=0}^{n-1}({\int }_{-1}^{1}b(t)dt)=1^n=1.$ Thus [F4] sends $[\omega ]$ to $1$.

For $n=1$ the product and Fubini iteration have one factor and recover $b(t)dt$. With the standard convention in dimension zero, the empty product is the value-one function on the positive point and also has integral one, although the displayed construction was stipulated for $n\ge 1$. Replacing any factor by zero makes the integral zero, as linearity predicts. There are no endpoints of the ambient manifold; the bounding-cube faces only delimit a zero extension. One explicitly constructed bump is reused finitely many times, so no choice principle enters.