State elimination preserves the language between every surviving state pair

Let $w\in P_{K\cup \{r\}}^G(p,q)$, witnessed by a path $p=s_0,s_1,\dots ,s_n=q$ whose intermediate states lie in $K\cup \{r\}$ and by a factorization $w=w_1\cdots w_n,w_j\in \mathcal{L}(\lambda (s_{j-1},s_j))\mathrm{.}$ Delete every occurrence of $r$ from the state list, keeping the surviving states in order: $p=t_0,t_1,\dots ,t_m=q\mathrm{.}$ For each consecutive pair $t_{j-1},t_j$, the deleted portion between them is either empty or consists of one entrance into $r$, zero or more $r$-to-$r$ loops, and one exit from $r$. Therefore the corresponding subword of $w$ lies in the language of the updated label ${\lambda }^{\mathrm{\prime }}(t_{j-1},t_j)$ from [L2]. Using the same surviving-state list and these compressed subwords gives a witness that $w\in P_K^{G\setminus r}(p,q)$.

Conversely, let $w\in P_K^{G\setminus r}(p,q)$, witnessed by a surviving-state path $p=t_0,t_1,\dots ,t_m=q$ with intermediate states in $K$ and by subwords in the denoted languages of the updated labels ${\lambda }^{\mathrm{\prime }}(t_{j-1},t_j)$. For each such subword, [L2] says that it is either an old direct $t_{j-1}$-to-$t_j$ word or a concatenation of an old $t_{j-1}$-to-$r$ word, finitely many old $r$-to-$r$ words, and an old $r$-to-$t_j$ word. Expanding every updated edge in this way inserts only the eliminated state $r$ between surviving states, so the resulting path in $G$ has all intermediate states in $K\cup \{r\}$. Hence $w\in P_{K\cup \{r\}}^G(p,q)$.

Steps 1.1 and 1.2 prove the two inclusions, so the two path languages are equal.