Compatibility of smooth atlases is an equivalence relation, and smooth Euclidean maps compose

Reflexivity and symmetry: $\mathcal{A}\cup \mathcal{A}=\mathcal{A}$ is an atlas, [F1, given] so $\mathcal{A}$ is compatible with itself; and compatibility is cross-pairwise over the two atlases, so interchanging $\mathcal{A}$ and $\mathcal{B}$ leaves the same cross-pair conditions.

Claim 2 for $r=0$: by [A1] a $C^0$ map is continuous, and $u$, being smooth, [given, A1, L3, L4, L5] has continuous first partials by [A1], is totally differentiable by [L3], and is continuous by [L4]; the composite is continuous by [L5]. The post-composition half is the same with $h$ and $v$.

Multiplication $\mu (a,b)=ab$ is totally differentiable at every point with [given, L6, L4] $D\mu (a,b)(s,t)=sb+at$: the difference $\mu (a+s,b+t)-\mu (a,b)-(sb+at)$ equals $st$, whose absolute value is at most the squared Euclidean norm of $(s,t)$, so the normalized remainder of [L6] tends to zero; hence $\mu$ is continuous by [L4].

Let $p,q:W\to \mathbb{R}$ be scalar $C^k$ maps. [step 1.3, L1, L2, L3, L5, A1] The case $k=0$ follows from step 1.3 and [L5], since $pq=\mu \circ (p,q)$ with both factors continuous. For $k\ge 1$, [L3] makes $(p,q)$ totally differentiable, [L1] applies to $\mu \circ (p,q)$, and [L2] gives ${\mathrm{\partial }}_i(pq)=({\mathrm{\partial }}_{i}p)q+p({\mathrm{\partial }}_{i}q)$. Induction on $k$ shows the right-hand side is $C^{k-1}$, so $pq$ is $C^k$ by [A1].

Finite sums of scalar $C^k$ functions are $C^k$: [step 2.1, A1] sums are handled by the additivity and homogeneity in [A1], and products by step 2.1.

Claim 2, for finite $r$, follows by induction on $r$. [step 1.2, step 3.1, L1, L2, L3, A1, given] The base case $r=0$ is step 1.2. For $r\ge 1$, the partials of each component $g_l$ are $C^{r-1}$ by [A1], so [L3] makes $g$ and $u$ totally differentiable and [L1], [L2] give ${\mathrm{\partial }}_i(g\circ u{)}_l={\sum }_j(({\mathrm{\partial }}_j{g}_l)\circ u)\cdot {\mathrm{\partial }}_i{u}_j$. The induction hypothesis makes each $({\mathrm{\partial }}_j{g}_l)\circ u$ of class $C^{r-1}$, smoothness of $u$ makes each ${\mathrm{\partial }}_i{u}_j$ of class $C^{r-1}$, and step 3.1 makes the sum $C^{r-1}$. With step 1.2 this proves $g\circ u$ is $C^r$ by [A1]. The post-composition half with $v\circ h$ is the same argument, and the case $r=\mathrm{\infty }$ follows by applying the finite case to every finite $r$.

For transitivity, let $\mathcal{A}\sim \mathcal{B}$ and [F1, step 4.1, choose] $\mathcal{B}\sim \mathcal{C}$. Fix charts $(U,\phi )\in \mathcal{A}$ and $(W,\chi )\in \mathcal{C}$, and let $p\in U\cap W$. Choose $(V,\psi )\in \mathcal{B}$ with $p\in V$, which exists because $\mathcal{B}$ covers $M$ by [F1]. On the open set $\phi (U\cap V\cap W)$ one has $\chi \circ {\phi }^{-1}=(\chi \circ {\psi }^{-1})\circ (\psi \circ {\phi }^{-1})$, so step 4.1 with $r=\mathrm{\infty }$ makes this transition smooth on a neighbourhood of $\phi (p)$.

Every point of $\phi (U\cap W)$ has such a neighbourhood, so [step 5.1, A1] $\chi \circ {\phi }^{-1}$ is smooth on all of $\phi (U\cap W)$ because the iterated partial derivatives exist and are continuous locally at every point. The same argument with the charts interchanged makes $\phi \circ {\chi }^{-1}$ smooth.

Thus every chart of $\mathcal{A}$ is compatible with every chart of [F1, step 1.1, step 4.1, step 6.1] $\mathcal{C}$, so $\mathcal{A}\cup \mathcal{C}$ is a smooth atlas by [F1]. This is exactly the transitivity of atlas compatibility. Together with step 1.1, compatibility of smooth atlases is an equivalence relation, and claim 2 was proved in step 4.1.