Regular-value formula for compact-support degree

The singleton $\{y\}$ is compact, so properness makes $K_y=F^{-1}(y)$ compact. At $p\in K_y$, [F3] makes $d{F}_p$ surjective, and equal finite dimensions make it invertible. By [F4] an inverse neighbourhood $O$ of $p$ meets $K_y$ only at $p$. The set of all such neighbourhoods, over all $p$ and all available branches, covers $K_y$ without a choice of branch at each point. A finite subcover from [F5] shows that $K_y$ is finite, since each member contains exactly one fibre point. Write its distinct points as $p_1,\dots ,p_m$, with $m=0$ allowed.

For the finitely many fibre points choose inverse branches and shrink their source domains to pairwise disjoint opens $O_i$. To do this, for every pair $p_i\mathrm{\ne }{p}_j$ choose disjoint Hausdorff neighbourhoods, and intersect the finitely many neighbourhoods belonging to each point with its original inverse domain. Each restriction is still a diffeomorphism onto an open set $W_i$ containing $y$. Shrink further so its orientation sign is the constant ${\epsilon }_i=\mathrm{sgn}(d{F}_{p_i})$ using [F10]. All these domains can lie inside their original source coordinate charts. There are only finitely many restrictions and pairwise separations.

Choose a target chart about $y$ and a closed coordinate ball $K$ centred at its coordinate, contained in the chart image, and of positive radius. Its inverse image under the chart is compact by [F7] and the continuous-image criterion [F5]; denote this compact neighbourhood also by $K$. Properness makes $F^{-1}(K)$ compact. Put $C=F^{-1}(K)\setminus {\bigcup }_{i=1}^m{O}_i\mathrm{.}$ This is a closed subset of the compact Hausdorff space $F^{-1}(K)$, so compact by [F6]. Its continuous image $F(C)$ is compact by [F5] and closed in $N$ by [F6], and it misses $y$ because all fibre points were in the $O_i$. Therefore $\mathrm{int}K\cap {\bigcap }_{i=1}^m{W}_i\setminus F(C)$ is an open neighbourhood of $y$; for $m=0$ omit the intersection. Choose a smaller coordinate ball $V$ about $y$ inside it. For $U_i=O_i\cap F^{-1}(V)$ we have diffeomorphisms $F{\mathrm{\mid }}_{U_i}:U_i\to V$, disjoint $U_i$, and $F^{-1}(V)={\coprod }_{i=1}^m{U}_i\mathrm{.}$ Indeed any preimage of $V$ lies in $F^{-1}(K)$ and cannot lie in $C$, so it lies in an $O_i$; the reverse containment is immediate. This compact-neighbourhood argument excludes additional branches approaching $y$ from far away.

By [F8] choose $\nu$ compactly supported in $V$ with integral one. For each $i$ define ${\beta }_i$ to equal $(F{\mathrm{\mid }}_{U_i}{)}^{\ast }(\nu {\mathrm{\mid }}_V)$ on $U_i$ and zero elsewhere. Its support is contained in the image of $\mathrm{supp}\nu$ under the continuous inverse branch, hence is compact in $U_i$ by [F5] and closed in $M$ by [F6]. Thus extension by zero is smooth: the formulas on $U_i$ and on the open complement of that compact set agree where both apply. The disjoint-union identity in step 3.1 gives the global finite equality $F^{\ast }\nu ={\sum }_i{\beta }_i$. Outside $F^{-1}(V)$ the pulled-back form is zero because $\nu$ vanishes outside $V$.

Choose a positive target chart $\psi :V\to B\subset {\mathbb{R}}^n$. On $U_i$ the map ${\varphi }_i=\psi \circ F$ is a smooth coordinate chart, and its orientation sign is ${\epsilon }_i$ by [F2], [F10] and step 2.1. If $\nu$ has coefficient $b$ in the $\psi$ chart, then ${\beta }_i$ has exactly the same coefficient $b$ in the ${\varphi }_i$ chart, by the definition of pullback and ${\varphi }_i=\psi F$. Both coefficients have compact support inside the common chart image $B$. Signed chart agreement and locality in [F9] therefore give ${\int }_M{\beta }_i={\epsilon }_i{\int }_{B}b(x)dx={\epsilon }_i{\int }_N\nu ={\epsilon }_i\mathrm{.}$ Finite linearity [F9], step 4.1 and [F1] now give $\mathrm{deg}(F)={\int }_M{F}^{\ast }\nu ={\sum }_{i=1}^m{\epsilon }_i\mathrm{.}$ This is an integer because it is a finite sum of $+1$ and $-1$. No unsigned chart sign or compact-support change-of-variables hypothesis is omitted: those comparisons are already part of the proved signed-chart integral [F9].

If $m=0$ in positive dimension, step 3.1 gives $F^{-1}(V)=\mathrm{\varnothing }$, so $F^{\ast }\nu =0$ and step 5.1 gives degree zero. For $n=0$, connectedness and nonemptiness make both manifolds singletons: every singleton in a zero-manifold is open, so two distinct points would separate it by a singleton and its complement. Their unique map has one-point fibre and the derivative between zero spaces is invertible. A normalized function on $N$ has value ${\epsilon }_N$, and its pullback integrates on $M$ to ${\epsilon }_M{\epsilon }_N$, precisely the sign [F2]. Thus the formula holds in dimension zero without using a positive-dimensional inverse function theorem. At $n=1$ the signs are those of the nonzero one-variable derivatives; compact supports stay inside the open branch intervals by step 4.1. Only the one fibre, finite branches and one bump are selected. The proof of [F4] uses its currently available choice-free completeness direction, and no AC, Sard theorem, or global partition is used.