Proof that a group is abelian. 
If $(G,*)$ is a group and $(a * b)^2 = a^2 * b^2$ then $(G, *)$ is abelian for all $a,b \in G$.

I know that I have to show $G$ is commutative, ie $a * b = b * a$
I have done this by first using $a^{-1}$ on the left, then $b^{-1}$ on the right, and I end up with and expression   $ab = b * a$. Am I mixing up the multiplication and $*$ somehow?
Thanks
 A: $abab=a^2b^2\implies a^{-1}abab=a^{-1}a^2b^2\implies bab=ab^2\implies bab b^{-1}= ab^2b^{-1}\implies ba=ab$
A: There is only one operation defined for the group, namely $*$, so if you want to be pedantic/exact, $a*b$ is a valid statement, while $ab$ is not defined.
However, in practice we shorten the notation, so $a*b$ can be written as $ab$.
So your final expression is equivalently $ab=ba$ or $a*b=b*a$. They are the same with slightly different notation.
A: In one side, $(a \ast b)^2 = a^2 \ast b^2$ (hypothesis). On the other side, $(a \ast b)^2 = a \ast b \ast a \ast b $. So: $$a^2 \ast b^2 = a \ast b \ast a \ast b \\ a \ast b = b \ast a $$
In groups there is only one operation, which we often think as multiplication. It could be well addition, or composition of functions, etc.
A: For notational ease, let's write $ab$ in place of $a*b$. This is ultimately, an application of left and right-cancellation in a group. Namely, $$(ab)^2=a^2b^2$$ and expanding each side we see that $$abab=aabb.$$ Canceling on the left we get $bab=abb$ and now canceling on the right we have that $ba=ab$. Hence, $G$ is abelian. 
A: Here's the proof that I got from Prover9:
1 G(x,y) = G(y,x) # label(non_clause) # label(goal).  [goal].
2 G(x,G(y,z)) = G(G(x,y),z).  [assumption].
3 G(G(x,y),z) = G(x,G(y,z)).  [copy(2),flip(a)].
4 G(x,N(x)) = 1.  [assumption].
5 G(x,1) = x.  [assumption].
6 G(G(x,y),G(x,y)) = G(G(x,x),G(y,y)).  [assumption].
7 G(x,G(y,G(x,y))) = G(x,G(x,G(y,y))).  [copy(6),rewrite([3(3),3(6)])].
8 G(c2,c1) != G(c1,c2).  [deny(1)].
9 G(x,G(N(x),y)) = G(1,y).  [para(4(a,1),3(a,1,1)),flip(a)].
12 G(x,G(y,G(x,G(y,z)))) = G(x,G(x,G(y,G(y,z)))).  [para(7(a,1),3(a,1,1)),rewrite([3(4),3(3),3(2),3(7),3(6)]),flip(a)].
19 G(1,N(N(x))) = x.  [para(4(a,1),9(a,1,2)),rewrite([5(2)]),flip(a)].
24 G(x,N(N(y))) = G(x,y).  [para(19(a,1),3(a,2,2)),rewrite([5(2)])].
26 G(1,x) = x.  [para(19(a,1),9(a,2)),rewrite([24(4),9(3)])].
31 G(x,G(N(x),y)) = y.  [back_rewrite(9),rewrite([26(5)])].
58 G(x,G(y,x)) = G(x,G(x,y)).  [para(4(a,1),12(a,1,2,2,2)),rewrite([5(2),4(4),5(4)])].
90 G(x,y) = G(y,x).  [para(31(a,1),58(a,2,2)),rewrite([3(3),31(4)])].
91 $F.  [resolve(90,a,8,a)].
