Converting generalized NFAs to NFAs I came across generalized nondeterministic finite automata (GNFAs) in Sipser's Introduction to the Theory of Computation. These are automata where transitions are labelled with regular expressions, rather than single symbols from the alphabet. I thought he would explain why GNFAs are allowed. I mean, an appropriate explanation would be that GNFAs are equivalent to NFAs, or GNFAs are equivalent to DFAs or some such argument. But I couldn't find any such explanation in the book. 

Online, I read in this article that you can convert a GNFA to an NFA as follows: 


  For each transition arrow in the GNFA, we insert the complete
  automaton accepting the language generated by the transition arrow’s
  label as a “subautomaton;” this way, we can replace each regular
  expression by a set of states and character transitions


How is the automaton inserted? 

Let's say we have a GNFA with an arrow going from state A to state B labelled with a regular expression R. To convert this GNFA to an NFA, do we get rid of that arrow, instead, take NFA N that recognizes L(R), and create an arrow from A to the start state of N labelled with the epsilon symbol, then create arrows from the accept states of N to B, each also labelled with the epsilon symbol? 

Of course the accept states of N would no longer be accept states in the new machine, would they? 

I know that GNFAs are equivalent to NFAs but I need a convincing proof, not just a short paragraph mentioning their equivalence.
You are correct in your understanding of the construction: For every transition arrow, say from state $A$ to state $B$ in the GNFA labeled by a regular expression $R$, you replace that transition by the NFA, $N$, for $R$, with an $\epsilon$-transition from $A$ to the start state of $N$ and $\epsilon$-transitions from the final states of $N$ (which you then "un-finalize") to state $B$. Do this for every transition in the GNFA and you'll wind up with an ordinary NFA. 

To show that the two accept the same language, it's enough to rely on the previous result (Lemma 1.55 in Sipser) that any regular expression denotes a language that is recognized by a NFA.