Block induction is transitive when both stages are defined

Put $b=c^H$ and $B=b^G$. By F1 there are split inclusions and retractions $i:c\to {\mathrm{Res}}_{K\times K}b$, $r$ back, and $j:b\to {\mathrm{Res}}_{H\times H}B$, $s$ back, with $ri=1_c$ and $sj=1_b$. Restricting $j,s$ to $K\times K$ retains their composite identity. Therefore $(\mathrm{Res}j)i$ and $r(\mathrm{Res}s)$ have composite $1_c$, exhibiting $c$ as a summand of ${\mathrm{Res}}_{K\times K}B$.

Since $c^G$ is defined, F1 makes it the unique global block with this summand property. Step 1.1 proves that $B$ has that property, so $c^G=B=(c^H{)}^G$. The same map composition works when two or all three groups coincide. The proof assumes the existence of all three blocks and does not deduce the third definedness from the first two. It composes finitely many given maps and uses no AC.