# Formal proof of the concatenation of two regular languages automaton

During an exercise for college, given two NFA's, $A_1\text{ and }A_2$ that accept the languages $L_1\text{ and }L_2$, I've built a NFA, $M$ that accepts the language $L_1*L_2$ (concatenation).

The formal NFA description is: $M = (Q, \Sigma, \delta, q_0, F)$ where

1. $Q = Q_1 \cup Q_2$
2. $\Sigma\$ is the same
3. $q_0 = q_0\ (\text{of }A_1)$
4. $F= F\ (\text{of }A_2)$
5. $\delta = \delta\ (\text{of }A_1)\cup \delta\ (\text{of }A_2)$
6. and for each state $q \in F\text{ of }L_1, \delta(q,\epsilon)= q_0\text{ of }L_2$

Now I need to formally prove that $L(M) = L(A1) * L(A2)$. Can I get a direction to start from?

-
The details will depend quite a bit on the specific formalism that you’re using for NFAs. –  Brian M. Scott Nov 15 '12 at 21:10
what do you mean? –  DanielY Nov 15 '12 at 21:31
You can’t give a formal proof unless you have a formal description of your NFAs. Not everyone uses quite the same formal description. What is yours? –  Brian M. Scott Nov 15 '12 at 21:35
edited my question, given there –  DanielY Nov 15 '12 at 21:42

As a hint, a common way of showing two sets, $A\text{ and }B$ are equal is to show that $A\subseteq B$ and that $B\subseteq A$. Depending on your construction of $M$ you shouldn't have much difficulty showing that, first, any word in $L(M)$ is in $L(A_1)*L(A_2)$ and, second, that any word in $L(A_1)*L(A_2)$ is accepted by your $M$.
Begin with "Let $w\in M$, then on $w, M$ will make transitions from its start state to its final state. However, by the construction of $M$ that will require ...". The point is that you can't have a proof that doesn't mention the structure of $M$. –  Rick Decker Nov 15 '12 at 22:18