Local orientation sign of a regular preimage

By regularity the tangent map is an isomorphism. Its top exterior power is an isomorphism of one-dimensional lines, so by [F3] it carries each ray bijectively to one of the two target rays. Exactly one is the chosen target ray, and the other is its negative. Thus exactly one of the two signs applies, using the actual orientation data from [F2].

For $n>0$, let $e$ and $f$ be positively oriented bases of the source and target tangent spaces. If $A$ is the matrix of $d{F}_p$ in them, then ${\bigwedge }^{n}d{F}_p(e_1\wedge \cdots \wedge e_n)=\det (A)f_1\wedge \cdots \wedge f_n\mathrm{.}$ The determinant is nonzero by invertibility, so its sign is precisely the ray comparison of step 1.1 and agrees with [F1]. If other positive bases have transition matrices $P,Q$, then the new matrix is $Q^{-1}AP$ and its determinant is $\det (A)\det (P)\mathrm{/}\det (Q)$. Both extra factors are positive by [F3]; hence the sign is independent of those bases or oriented charts.

For $n=0$, [F3] identifies both determinant lines with $\mathbb{R}$ and the induced map with the identity. Their chosen rays are represented by ${\epsilon }_M(p)$ and ${\epsilon }_N(y)$. The image of the first is a positive multiple of the second exactly when the signs coincide; otherwise it is a negative multiple. Thus the sign is their product. In dimension one, step 2.1 is the sign of the single nonzero derivative in positive coordinates. A singular point is excluded, so zero determinants receive no sign here. If a regular fibre is empty there is no point to label, not a choice of labels; at a given point the label is uniquely determined. No compactness, properness, boundary endpoint condition or choice axiom is needed for this local definition.