[proofplan] We prove $\mathcal{L}(G) = \mathcal{L}(G')$ by showing each inclusion separately; by the symmetry furnished by the inverse isomorphism $f^{-1}$ it suffices to establish $\mathcal{L}(G) \subseteq \mathcal{L}(G')$. Given $w \in \mathcal{L}(G)$, we fix a $G$-derivation of $w$ from the start symbol $S$ and apply the extension $\hat{f}: \Omega^\star \to \Omega'^\star$ letterwise to each intermediate string. The isomorphism conditions guarantee that (a) the derivation begins at $S' = \hat{f}(S)$, (b) each single-step reduction is preserved because each rule of $G$ maps to a rule of $G'$, and (c) the final word is fixed because $f$ is the identity on terminals. Hence $\hat{f}$ maps a $G$-derivation of $w$ to a $G'$-derivation of $w$, so $w \in \mathcal{L}(G')$. [/proofplan] [step:Reduce to proving one inclusion by symmetry] Let $f: \Omega \to \Omega'$ be a grammar isomorphism from $G = (\Omega, N, S, P)$ to $G' = (\Omega', N', S', P')$, where $\Omega = T \sqcup N$ and $\Omega' = T' \sqcup N'$ are the partitions of the alphabets into terminals and non-terminals. By definition of grammar isomorphism, the inverse map $f^{-1}: \Omega' \to \Omega$ is a grammar isomorphism from $G'$ to $G$. Hence if we establish the implication \begin{align*} \mathcal{L}(G) &\subseteq \mathcal{L}(G') \qquad \text{whenever $G$ and $G'$ are isomorphic}, \end{align*} applying it to the pair $(G', G)$ with isomorphism $f^{-1}$ gives $\mathcal{L}(G') \subseteq \mathcal{L}(G)$, and the two inclusions combine (by antisymmetry of $\subseteq$) to $\mathcal{L}(G) = \mathcal{L}(G')$. We therefore fix $w \in \mathcal{L}(G)$ and prove $w \in \mathcal{L}(G')$. [/step] [step:Extract a $G$-derivation of $w$ and extend $f$ to strings] Since $w \in \mathcal{L}(G)$, there exist $n \geq 0$ and a finite sequence \begin{align*} S = \sigma_0 \xrightarrow{G}_1 \sigma_1 \xrightarrow{G}_1 \sigma_2 \xrightarrow{G}_1 \cdots \xrightarrow{G}_1 \sigma_n = w, \end{align*} where each $\sigma_i \in \Omega^\star$ and each arrow denotes a single-step $G$-reduction; moreover $w \in T^\star$ since $w \in \mathcal{L}(G)$ consists only of terminals. Extend $f$ letterwise to finite strings by \begin{align*} \hat{f}: \Omega^\star &\to \Omega'^\star \\ (a_1, a_2, \dots, a_k) &\mapsto (f(a_1), f(a_2), \dots, f(a_k)), \end{align*} with $\hat{f}(\varepsilon) := \varepsilon'$ (the empty string in $\Omega'^\star$). The map $\hat{f}$ is a [monoid homomorphism](/page/???) with respect to concatenation: for $u, v \in \Omega^\star$, \begin{align*} \hat{f}(uv) &= \hat{f}(u) \hat{f}(v). \end{align*} [/step] [step:Verify the endpoints of the image derivation are $S'$ and $w$] We record the two endpoint identities. By isomorphism condition (2), $f$ maps the start symbol to the start symbol: $f(S) = S'$. Since $S \in \Omega^\star$ is a single-letter string, \begin{align*} \hat{f}(\sigma_0) &= \hat{f}(S) = f(S) = S'. \end{align*} By isomorphism condition (1) (or the corresponding condition that $f$ is the identity on terminals), $f|_T = \operatorname{id}_T$, i.e., $f(t) = t$ for every $t \in T$. Since $w = \sigma_n \in T^\star$, letterwise application gives \begin{align*} \hat{f}(\sigma_n) &= \hat{f}(w) = w. \end{align*} In particular $\hat{f}(w) \in T'^\star$ because each letter of $w$ lies in $T \subseteq T'$ (more precisely, $f(T) \subseteq T'$ by the same condition, and $f|_T = \operatorname{id}$ means the image of each terminal of $G$ is the same symbol regarded as a terminal of $G'$). [/step] [step:Show that single-step reductions are preserved under $\hat{f}$] Fix $i \in \{0, 1, \dots, n-1\}$. The single-step reduction $\sigma_i \xrightarrow{G}_1 \sigma_{i+1}$ means there exist $\alpha, \beta \in \Omega^\star$ and a rule $(\gamma \to \delta) \in P$ such that \begin{align*} \sigma_i &= \alpha \gamma \beta, \\ \sigma_{i+1} &= \alpha \delta \beta. \end{align*} Applying the homomorphism $\hat{f}$ to both strings, \begin{align*} \hat{f}(\sigma_i) &= \hat{f}(\alpha) \hat{f}(\gamma) \hat{f}(\beta), \\ \hat{f}(\sigma_{i+1}) &= \hat{f}(\alpha) \hat{f}(\delta) \hat{f}(\beta). \end{align*} By isomorphism condition (4) (preservation of rules), the pair $(\hat{f}(\gamma) \to \hat{f}(\delta))$ is a rule of $G'$, i.e., $(\hat{f}(\gamma) \to \hat{f}(\delta)) \in P'$. Hence the display above witnesses a single-step $G'$-reduction: \begin{align*} \hat{f}(\sigma_i) &\xrightarrow{G'}_1 \hat{f}(\sigma_{i+1}). \end{align*} [guided] The argument uses two structural facts in tandem. First, that $\hat{f}$ is a concatenation homomorphism, so it commutes with the decomposition $\sigma_i = \alpha\gamma\beta$: the surrounding context $\alpha$ and $\beta$ is carried through unchanged (up to the image), and the active rule-portion $\gamma$ is replaced by $\hat{f}(\gamma)$. Second, that the isomorphism condition (4) — "every rule of $G$ maps to a rule of $G'$" — guarantees that the replaced portion $\hat{f}(\gamma) \to \hat{f}(\delta)$ is a legitimate rule in $P'$. Together these reconstruct a single-step reduction in $G'$ from a single-step reduction in $G$. Without condition (4), the image of a rule might not be a rule in $G'$, and the pair $(\hat{f}(\gamma), \hat{f}(\delta))$ could sit outside $P'$, breaking the derivation. Without the homomorphism property, we could not split $\hat{f}(\alpha\gamma\beta)$ as $\hat{f}(\alpha)\hat{f}(\gamma)\hat{f}(\beta)$ and would have no way to locate the rule application inside the image string. [/guided] [/step] [step:Assemble a $G'$-derivation of $w$ from $S'$ and conclude] Concatenating the single-step reductions from the previous step and using the endpoint identities of the third step, we obtain \begin{align*} S' = \hat{f}(\sigma_0) \xrightarrow{G'}_1 \hat{f}(\sigma_1) \xrightarrow{G'}_1 \cdots \xrightarrow{G'}_1 \hat{f}(\sigma_n) = w. \end{align*} This is a $G'$-derivation of $w$ from $S'$ with every intermediate string in $\Omega'^\star$, so $w \in \mathcal{L}(G')$. By the reduction in the first step (applied to the isomorphism $f^{-1}$), the reverse inclusion $\mathcal{L}(G') \subseteq \mathcal{L}(G)$ also holds. Antisymmetry of $\subseteq$ gives \begin{align*} \mathcal{L}(G) &= \mathcal{L}(G'), \end{align*} as required. [/step]