Here is the grammar given on the wikipedia:
$$ S \rightarrow T \;|\; U \\ T \rightarrow VaT \;|\; VaV \;|\; TaV \\ U \rightarrow VbU \;|\; VbV \;|\; UbV \\ V \rightarrow aVbV \;|\; bVaV \;|\; \epsilon $$
I can understand how $V$ generates strings with equal number of a's and b's. I want to prove that $T$ generates strings with more a's than b's. The case for U can be proven symmetrically.
Here is my attempt and doubt.
$P(0)$: Suppose $s$ is a string with one extra a. Let $s_1$ be the longest balanced prefix of s. Then $s=s_1 t$ where t necessarily starts with $'a'$. For otherwise t will have a non-empty balanced prefix and $s_1$ won't be the longest prefix. Hence $s = s_1 a s_2$ where $s_1$ and $s_2$ are balanced and derivable from $V$. hence s can be derived as $S \rightarrow VaV=>^* s_1as_2$.
$P(n)$ : Suppose $T =>^* w$, where w has $n$ extra a's than b's. Let s be a string with $n+1$. Let $s_1$ and $t$ be as above. Then $t = aw$. By construction, $w$ has $n$ extra a's and is derivable from T. Therefore $T \rightarrow VaT =>^* s_1aw$.
My doubt is what is the need for the rule $T \rightarrow TaV$
