Language equivalence of Turing machines is undecidable

Fix once and for all a coded deterministic machine $A$ that accepts every input. Given an instance $⟨<mi\; mathvariant="normal">⌜</mi>M<mi\; mathvariant="normal">⌝</mi>,\widehat{w}⟩$ of $HAL{T}_{TM}$, use [L2] to build a machine $E_{M,w}$ that ignores its own input, simulates $M$ on $w$, accepts every input if that simulation ever halts, and otherwise loops forever on every input.

If $M$ halts on $w$, then every input to $E_{M,w}$ eventually triggers acceptance, so [L1] gives $L(E_{M,w})={\mathrm{\Sigma }}^{\ast }$. If $M$ does not halt on $w$, then $E_{M,w}$ accepts no input at all, so $L(E_{M,w})=\mathrm{\varnothing }$. Therefore $⟨<mi\; mathvariant="normal">⌜</mi>M<mi\; mathvariant="normal">⌝</mi>,\widehat{w}⟩\in HAL{T}_{TM}⟺⟨<mi\; mathvariant="normal">⌜</mi>E_{M,w}<mi\; mathvariant="normal">⌝</mi>,<mi\; mathvariant="normal">⌜</mi>A<mi\; mathvariant="normal">⌝</mi>⟩\in E{Q}_{TM}$.

Suppose for contradiction that $E{Q}_{TM}$ were decidable. Then step 2.1 would let that decider decide $HAL{T}_{TM}$, contradicting [L3]. Hence $E{Q}_{TM}$ is undecidable, by [L4].