Thom and Gysin constructions respect pullback and composition

In an orientation-preserving pullback square, [F1] identifies the pulled-back Thom class. Pullback commutes with ${\pi }^{\ast }$, relative cup product and the relative-to-absolute pair map, so the Thom isomorphism and [F3]'s Gysin map commute. Pulling back along the zero section gives Euler naturality, and [F4] supplies the resulting natural ladder of exact sequences.

For the composable zero sections, functoriality in [F4] identifies the restriction of the second normal bundle to $B$ as $s_{\xi }^{\ast }\eta$. The supplied iterated tubular identification orders the first normal directions as those of $\xi$ and the second as those of $s_{\xi }^{\ast }\eta$, hence identifies the composite normal bundle with $\xi \oplus s_{\xi }^{\ast }\eta$.

Apply [F3] twice to $a\in H^{\ast }(B;R)$. Under the iterated pair identification, the result is the relative-to-absolute image of ${\pi }^{\ast }a$ cupped first with $u_{\xi }$ and then with the pullback of $u_{\eta }$. Associativity makes this cup product ${\pi }^{\ast }a⌣(u_{\xi }⌣u_{s_{\xi }^{\ast }\eta })$. By [F1]–[F2], the parenthesized class is the Thom class of the ordered normal sum from step 1.2, so [F3] identifies the result with $(s_{\eta }\circ s_{\xi }{)}_{!}(a)$.

Empty bases and zero rings give unique zero maps. A rank-zero section with supplied orientation unit $o$ has Thom class and Euler class $o$ and acts by multiplication by $o$, by [F3]; this is the identity for the standard unit orientation. If either rank is zero, the ordered-sum formula of [F2] multiplies the corresponding orientation units, exactly as does the composite in step 2.1; ranks one and point bases require no change. Identity pullback squares, zero inputs, both orders of the normal sum, both stages of the composite, and every Gysin-sequence endpoint are covered by steps 1.1–2.1. Reversing the order would introduce the Koszul sign from [F2], which is why the order is stated. AC is used exactly through [A1]; the two-stage calculation is finite and makes no choices.