Lefschetz-Hopf index formula

By [F1] isolation and compactness make the fixed set finite. Choose pairwise disjoint admissible balls isolating its points. Applying [F2] successively in these balls yields a smooth map $g$ homotopic to $f$, unchanged outside the balls, with every fixed point nondegenerate and $I(g)=I(f)$. There are no additional fixed points outside the balls because $g=f$ there, and the finite index sum is defined by Geometric Lefschetz number (index sum).

Each connected component $C$ is carried by $g$ into a single component, since its image is connected. If that component is $C$, [F3] applies to the self-map $g{\mathrm{\mid }}_C$ and gives $I(g{\mathrm{\mid }}_C)=L(g{\mathrm{\mid }}_C)$. If it is a different component, $C$ has no fixed points, and the source-to-$C$ diagonal block of $g_{\ast }$ on the homology direct sum in [F4] is zero. Thus that component contributes zero both to the index sum and to the trace. Summing the finitely many diagonal-block identities gives $I(g)=L(g)$.

Since $f$ and $g$ are homotopic, [F4] gives $L(f)=L(g)$. Combining with the preceding steps gives $I(f)=I(g)=L(g)=L(f)$. AC is inherited from the finite-dimensional Lefschetz-number and twisted diagonal suppliers; the perturbations and the finite component decomposition require no global orientation or lift of either map.