Homotopy-cardinality pushforward satisfies base change

Fix a component $x\in {\pi }_0(X)$ and put $y=f(x)$. The homotopy fiber of $u^{\mathrm{\prime }}$ over $x$ is the pullback of the homotopy fiber of $u$ over $y$, hence is equivalent to it by the homotopy-cartesian condition. Since $u$ is proper, this fiber has finitely many components; therefore $u^{\mathrm{\prime }}$ is proper on components.

Fix $y^{\mathrm{\prime }}\in {\pi }_0(Y^{\mathrm{\prime }})$ and put $y=u(y^{\mathrm{\prime }})$. The homotopy fiber of $f^{\mathrm{\prime }}$ over $y^{\mathrm{\prime }}$ is equivalent to the homotopy fiber of $f$ over $y$, with its map to $X$ equal to the composite of the fiber map to $X^{\mathrm{\prime }}$ and $u^{\mathrm{\prime }}$. Thus the summands, their higher homotopy groups, and the values of $\alpha$ pulled back along $u^{\mathrm{\prime }}$ agree term by term. Both sides evaluated at $y^{\mathrm{\prime }}$ are the same finite sum from [F1].