I'm having trouble to formalize in FOL with equality, the statement
"Every element has a multiplicative inverse" or
"For every $x$ there's a $y$ such that $xy = e$ where $e$ is some identity.
The problems comes in with the identity. I tried to formalize as $ \forall x(\exists y( xy = x \wedge yx = x) \rightarrow \exists z(xz = y \wedge zx = y))$
is that correct?