Finite-CW real bundles have orthogonal complements under AC

If $X$ is empty, the claim is vacuous; assume it is nonempty. Each closed cell of $X$ is the continuous image of a closed disk and hence compact. Since there are finitely many cells, $X$ is a finite union of compact closed-cell images, so it is compact; [F1] gives Hausdorffness.

By [F2] and step 1.1, $X$ is paracompact and Hausdorff. The bundle's local trivializations form an open cover of $X$. Compactness gives a finite subcover. Apply [F3] to this cover: its AC and DC hypotheses hold because AC is given and [F4] derives DC. The resulting locally finite partition has only finitely many nonzero members: choose for each point a neighborhood meeting finitely many supports, then take a finite subcover of those neighborhoods by compactness; the union of the finite index sets is finite. Thus the chart subcover and partition give a finite numeration.

Apply [F5] to this finite numeration. It supplies a fiberwise-linear embedding $E\hookrightarrow X\times {\mathbb{R}}^N$ and the subbundle $F$ orthogonal to its image in the standard Euclidean metric. The fiberwise orthogonal direct sum is the whole trivial bundle, so $E\oplus F\cong X\times {\mathbb{R}}^N$. AC is used to obtain the partition in [F3] and, through [F4], to discharge its DC hypothesis in step 2.1.