Using induction to prova a regular expression belongs to the language generated by a grammar (well half-proving anyways) I have a grammar with this productions

S->aBSBBa |$ \epsilon $
  B->bB|$\epsilon$

$L(B)=b^*$ (by Arden's rule) and seems that $L(S) = a(b+ab^*a)^*a + \epsilon$
I have to prove that last statement. So I have to prove
1) $L(S)\subseteq a(b+ab^*a)^*a + \epsilon $
2) $a(b+ab^*a)^*a + \epsilon \subseteq L(S)$
For the first one i was thinking about using rule induction (not the purpose of the question so moving on)
For the second statement i was thinking about proving it by induction on $a(b+ab^*a)^na + \epsilon $ (if this is possible)  


*

*Basis step $n=0$
$ aa \in L(S)$
$
\epsilon \in L(S)
$

*Step - assuming $a(b+ab^*a)^na + \epsilon \subseteq L(S)$ i have to prove that is true for $n+1$
I have that $a(b+ab^*a)^n(b+ab^*a)a + \epsilon \subseteq L(S)$
so it it either $a(b+ab^*a)^nba + \epsilon \subseteq L(S)$
or $a(b+ab^*a)^nab^*aa + \epsilon \subseteq L(S)$
From this point I'm stuck i don't know how to prove those last two statements are true using the induction hypothesis (so that the hypothesis is true for all n)
Maybe I'm taking the wrong approach at the problem, any kind of help would be much appreachiated. Thanks


Edit: I'm starting to think that the regular expression is better written like
$(a(b+ab^*a)^*a)^*$ i don't know if the epsilon is allowed in regular expression.
Still, the problem about proving it remains, now it's even more complicated with the second kleene' star.
 A: I think that your regular expression may make the proof harder than necessary.
Since, as you say, $L(B)=b^*$, the production $S\to aBSBBa\mid\epsilon$ is effectively $S\to ab^*Sb^*a\mid\epsilon$. Suppose that we apply the first alternative $n$ times for some $n\ge 1$ and then apply the second; since $b^*b^*=b^*$, we get
$$(ab^*)^n(b^*a)^n=\underbrace{ab^*ab^*\ldots a}_{n\;a\text{’s}}b^*\underbrace{a\ldots b^*ab^*a}_{n\;a\text{’s}}\;.\tag{1}$$
This is a string of $2n$ $a$s, beginning and ending with $a$, with arbitrary numbers of $b$s between adjacent $a$s. We can think of it as 
$$(ab^*ab^*)^{n-1}ab^*a\;.$$
Finally,
$$L(S)=\sum_{n\ge 1}(ab^*ab^*)^{n-1}ab^*a+\epsilon=(ab^*ab^*)^*ab^*a+\epsilon\;.$$
This gives you a regular expression that is built up in a slightly simpler way.
A slightly less obvious alternative is to rewrite $(1)$ as
$$a(b^*ab^*ab^*)^{n-1}a\;,$$
taking advantage of the fact that $b^*b^*=b^*$. Then we have
$$L(S)=\sum_{n\ge 1}a(b^*ab^*ab^*)^{n-1}a+\epsilon=a(b^*ab^*ab^*)^*a+\epsilon\;;$$
considering the form of the $S$ production, this is probably easier to work with.
See if you can manage the proof with one or the other of these regular expressions.
