Let $\newcommand{\perm}[1]{\left\langle #1 \right\rangle}A = \perm{ Q, \Sigma, \delta, q_0, F }$ be a finite, nondeterministic automaton and $G(A) = \perm{ \Sigma, V, P, S }$ the grammar generated by it. I would like to show (with induction) that the languages $\newcommand{\lang}{\mathcal{L}} \lang(A)$ and $\lang(G(A))$ are the same.
A few definitions
To begin, the language generated by a grammar $G$, $\lang(G)$, is defined as $$ \newcommand{\set}[1]{\left\{ #1 \right\}} \newcommand{\derive}{\Longrightarrow} \lang(G) = \set{ x \in \Sigma^* \mid S \derive_G^+ x }, $$ as in the words in $\lang(G)$ should be derivable from the starting variable $S$ via the productions $P$ of the grammar in question. Secondly, a grammar $G$ can be generated from an automaton $A$ by taking these 4 steps:
Create a one-to-one mapping between the states $Q$ of the automaton $A$ and the variables or non-terminal symbols $V$ of the grammar $G$, for example $q_i\mapsto V_i$ (or simply use the states $q_i$ as the variables of the grammar).
Generate a production $\newcommand{\rewrite}{\longrightarrow} q_i \rewrite \alpha_jq_k$ for every state transition $\perm{q_i, \alpha_j} \mapsto q_k$ defined by the transition function $\delta$.
If the state $q_k$ is an accepting state, as in $q_k\in F$, create the production $q_i\rewrite \alpha_j$ instead of the one in item 2.
If the automaton accepts the empty string $\epsilon$, as in the initial state $q_0\in F$, also add the production rule $q_0\rewrite \epsilon$ to the set of productions $P$.
This grammar $G(A)$ is regular by definition, as all of its production rules are in the set \begin{align} V_i &\rewrite \alpha V_j \\ V_i &\rewrite V_j \\ V_i &\rewrite \alpha \quad\text{or} \\ V_i &\rewrite \epsilon \end{align} for $V_i, V_j \in V$ and $\alpha \in \Sigma$. The transformation in the direction of the automaton is done by directly reversing the steps 1--4.
The problem
What exactly should I induce upon? Should I take two automata $A_1$ and $A_2$, the regular grammars $G_1 = G(A_1)$ and $G_2 = G(A_2)$ generated from them by the procedure defined above, and assume that in both cases the languages generated by them are the same? But then in the induction step I'd somehow need to create a more complicated automaton $A_3$ and the grammar $G_3 = G(A_3)$ from these and show that the structure, in this case the fact that the languages $\lang(G_3)$ and $\lang(A_3)$ are the same, is preserved.
Is my idea of an induction hypothesis applicable here, and if it is, how is the more complicated automaton constructed in order for the proof to be exhaustive? I'm still very much struggling with the idea of structural induction.