The de Rham map is a cochain map without Stokes on simplices

Directly from the definitions of the singular coboundary and integration cochain, $(\delta I^k(\omega ))(\sigma )=I^k(\omega )(\mathrm{\partial }\sigma )={\int }_{\mathrm{\partial }\sigma }\omega ,$ while $I^{k+1}(d\omega )(\sigma )={\int }_{\sigma }d\omega \mathrm{.}$ Consequently the cochain-map equality evaluated on this one simplex is precisely ${\int }_{\mathrm{\partial }\sigma }\omega ={\int }_{\sigma }d\omega$, with the alternating face orientations built into $\mathrm{\partial }\sigma$.

Thus simplex Stokes implies the cochain identity by linearity over finite chains, and conversely the cochain identity for every $\omega$ and every simplex implies every one of these Stokes identities by step 1.1. This is the identity asserted in [F1]. The zero form, a degenerate simplex, $k=0$, and an empty manifold merely give special instances of the same equality; they do not establish the general claim. Hence omitting simplex Stokes (or a result logically equivalent to all its instances) leaves the cochain-map assertion unproved. No choice principle is involved.