Nice! Thanks, Plato.
I still am not able to follow the Double inverse theorem... maybe you could help make it clearer.
Let $\displaystyle *$ be an associative binary operation on a set $\displaystyle A$ with identity $\displaystyle e$, and let $\displaystyle x\in A$. If $\displaystyle x$ is invertible for $\displaystyle *$, let [tex]x^{-1}[/math denote the (unique) inverse for $\displaystyle x$. Then $\displaystyle x^{-1}$ is invertible and $\displaystyle (x^{-1})^{-1} = x$.
Proof: If $\displaystyle y$ is the inverse for $\displaystyle x$, then
$\displaystyle y*x=e=x*y$.
But this is exactly the condition for $\displaystyle x$ to be the inverse for $\displaystyle y$.
What confuses me about that proof is the last statement. I don't understand how that is sufficient.