[proofplan]
We establish the chain of isomorphisms $W(K^{\mathrm{ab}}/K) \cong W(K^{\mathrm{ur}} L/K) \cong W(K^{\mathrm{ur}}/K) \times \operatorname{Gal}(L/K) \cong \operatorname{Frob}_K^{\mathbb{Z}} \times \operatorname{Gal}(L/K)$ by three steps: the first isomorphism uses the preceding lemma to identify $K^{\mathrm{ab}}$ with $K^{\mathrm{ur}} L$; the second uses the fact that $K^{\mathrm{ur}} \cap L = K$ (since $L/K$ is totally ramified and $K^{\mathrm{ur}}/K$ is unramified) to decompose the Weil group of a compositum; and the third identifies the Weil group of the unramified extension with the cyclic group generated by the Frobenius.
[/proofplan]
[step:Establish the first isomorphism $W(K^{\mathrm{ab}}/K) \cong W(K^{\mathrm{ur}} L/K)$]
By the preceding lemma (referenced in the theorem statement), $K^{\mathrm{ab}} = K^{\mathrm{ur}} L$. Therefore
\begin{align*}
W(K^{\mathrm{ab}}/K) = W(K^{\mathrm{ur}} L / K).
\end{align*}
This is an equality rather than merely an isomorphism: the Weil group is defined relative to the extension, and since the extensions coincide, so do their Weil groups.
[/step]
[step:Decompose $W(K^{\mathrm{ur}} L / K) \cong W(K^{\mathrm{ur}}/K) \times \operatorname{Gal}(L/K)$ using linear disjointness]
Since $L/K$ is totally ramified and $K^{\mathrm{ur}}/K$ is unramified, the extensions are linearly disjoint over $K$: $K^{\mathrm{ur}} \cap L = K$. To verify this, suppose $x \in K^{\mathrm{ur}} \cap L$. Then $x/K$ is both unramified (as a subextension of $K^{\mathrm{ur}}/K$) and totally ramified (as a subextension of the totally ramified $L/K$). An extension that is simultaneously unramified and totally ramified must be trivial: if $K(x)/K$ has ramification index $e = [K(x):K]$ (totally ramified) and residue degree $f = [K(x):K]$ (unramified), then $[K(x):K] = ef$ forces $e = f = 1$, so $x \in K$.
Linear disjointness gives
\begin{align*}
\operatorname{Gal}(K^{\mathrm{ur}} L / K) \cong \operatorname{Gal}(K^{\mathrm{ur}}/K) \times \operatorname{Gal}(L/K).
\end{align*}
The Weil group $W(K^{\mathrm{ur}} L / K)$ consists of those $\sigma \in \operatorname{Gal}(K^{\mathrm{ur}} L / K)$ whose restriction to $K^{\mathrm{ur}}$ is an integer power of $\operatorname{Frob}_K$. Under the product decomposition, this condition involves only the first factor, so
\begin{align*}
W(K^{\mathrm{ur}} L / K) = W(K^{\mathrm{ur}}/K) \times \operatorname{Gal}(L/K).
\end{align*}
[guided]
The Weil group $W(E/K)$ for an extension $E \supseteq K^{\mathrm{ur}}$ is defined as the preimage of $\operatorname{Frob}_K^{\mathbb{Z}} \subseteq \operatorname{Gal}(K^{\mathrm{ur}}/K)$ under the restriction map $\operatorname{Gal}(E/K) \to \operatorname{Gal}(K^{\mathrm{ur}}/K)$. Under the product decomposition $\operatorname{Gal}(K^{\mathrm{ur}} L/K) \cong \operatorname{Gal}(K^{\mathrm{ur}}/K) \times \operatorname{Gal}(L/K)$, the restriction to $K^{\mathrm{ur}}$ is just the projection onto the first factor. So the preimage of $\operatorname{Frob}_K^{\mathbb{Z}}$ is $\operatorname{Frob}_K^{\mathbb{Z}} \times \operatorname{Gal}(L/K)$, where we identify $\operatorname{Frob}_K^{\mathbb{Z}}$ with its preimage $W(K^{\mathrm{ur}}/K)$ in the first factor.
The fact that the full second factor $\operatorname{Gal}(L/K)$ appears (without any restriction) is because $L/K$ is totally ramified, so $L \cap K^{\mathrm{ur}} = K$, and every element of $\operatorname{Gal}(L/K)$ extends to $K^{\mathrm{ur}} L$ by acting directly on $K^{\mathrm{ur}}$. Such an extension automatically restricts to $\operatorname{id} \in \operatorname{Gal}(K^{\mathrm{ur}}/K)$, which is $\operatorname{Frob}_K^0$, an integer power of $\operatorname{Frob}_K$.
[/guided]
[/step]
[step:Identify $W(K^{\mathrm{ur}}/K) \cong \operatorname{Frob}_K^{\mathbb{Z}}$]
By definition, the Weil group of the unramified extension $K^{\mathrm{ur}}/K$ is
\begin{align*}
W(K^{\mathrm{ur}}/K) = \{\sigma \in \operatorname{Gal}(K^{\mathrm{ur}}/K) : \sigma|_{K^{\mathrm{ur}}} \in \operatorname{Frob}_K^{\mathbb{Z}}\} = \operatorname{Frob}_K^{\mathbb{Z}}.
\end{align*}
The second equality is the tautological case: restricting to $K^{\mathrm{ur}}$ is the identity map on $\operatorname{Gal}(K^{\mathrm{ur}}/K)$, so the condition is simply $\sigma \in \operatorname{Frob}_K^{\mathbb{Z}}$.
Combining all three steps:
\begin{align*}
W(K^{\mathrm{ab}}/K) \cong W(K^{\mathrm{ur}} L/K) \cong W(K^{\mathrm{ur}}/K) \times \operatorname{Gal}(L/K) \cong \operatorname{Frob}_K^{\mathbb{Z}} \times \operatorname{Gal}(L/K).
\end{align*}
[/step]
