How to deduce this equation? First of all, sorry for posting an image instead of typing.

What the book says is:
Given the signature (S,Σ) with the associated sorts (S), functions (Σ) and the equations (E), show that E ⊢ ($\forall${$x$}) $(x^{-1})^{-1}$ = $x$.
I can't find any way to demonstrate that. I tried all types of combinations where I would substitute with $e$, $e^{-1}$, $x^{-1}$, $(x^{-1})^{-1}$, but nothing worked out.
Any help is appreciated.
 A: I believe that I should not give a complete answer. The proof is tricky, but there are many such proofs in abstract mathematics. They look like game of symbols (Hilbert). Whether you find sense or joy in it depends on you.
When doing proofs in abstract algebra, I use a technique which I call “2 reaction paths”. Reactions like in chemistry. Example. Let $e_<$ be left neutral and $e_>$ be right neutral. $e_<\circ e_> $ reacts in 2 ways: $e_<$ disappears because it is on the left side, or $e_>$ disappears because it is on the right side. We obtain a new identity $e_<=e_> $. Example. Let $b_<$ be a left inverse of $a$ and $b_>$ be a right inverse of $a$. $b_<\circ a\circ b_> $ reacts in 2 ways: $b_<\circ a$ disappears, or $a\circ b_>$ disappears. We obtain a new identity $b_<=b_> $.
A stronger version of your theorem is as follows. If $\circ $ is associative, $\forall x(e\circ x = x) $ ($e$ is left neutral), and $\forall x(x^{-1}\circ x = e) $ ($x^{-1}$ is a left inverse of $x$), then this is a group. The proof starts as follows. $x^{-1}$ reacts on the right side with $x$. Can $x^{-1}$ react on the left side? With what? Look at the axioms. If you obtain a new identity, use it again with the technique. You need to prove that $e$ is right neutral. $\forall x((x^{-1})^{-1}\circ x = e) $ will fall out as a side effect. You can find a complete proof in a textbook “Abstract Algebra” by Claudia Menini and Freddy Van Oystaeyen, Theorem 9.7. Their proof contains no explanation though.
