The following are axioms and theorems of group theory:
Axiom 1: $(\forall x)(\forall y)(\forall z)(x \, \circ\,(y\, \circ \,z) = (x \, \circ \,y)\,\circ\,z)$
Axiom 2: $(\forall x)(x \, \circ \, e = x)$
Axiom 3: $(\forall x)(x \, \circ \, x^{-1} = e) $
Theorem 1 (Right hand cancellation):
$$(\forall x)(\forall y)(\forall z)(x \, \circ \, z \, = \, y \, \circ \,z \, \rightarrow \, x = y)$$
Theorem 2 (Commutativity of Identity): $$(\forall x)(x \, \circ \, e \, = \, e \, \circ \, x)$$
Theorem 3 (Uniqueness of Identity):
$$(\forall y)[(\forall x)(x \, \circ \, y \, = \, x) \rightarrow \, y \, = \, e]$$
Theorem 4 (Commutativity of Inverse):
$$(\forall x)(x \, \circ \, x^{-1}= \, x^{-1} \circ \, x)$$
Theorem 5 (Left-hand cancellation):
$$(\forall x)(\forall y)(\forall z)(z \, \circ \, x \, = \, z \, \circ \,y \, \rightarrow \, x = y)$$
Theorem 6 (Uniqueness of Inverse):
$$(\forall x)(\forall y)(x \, \circ \, y \, = e \rightarrow y=x^{-1})$$
Theorem 7 (idk the name):
$$(\forall x)((x^{-1})^{-1}=x)$$
With only these, I'm asked to prove the theorem:
$$(\forall x)(\forall y)(\exists z)(x = y\,\circ\,z)$$
In my attempt I start with none of the axioms and theorems but rather I try to use the fact that all valid interpretations of the operator, $\circ$, satisfies the closure property. That is, I start with the statement
$(\forall x)(\forall y)(\exists z)(x \,\circ\,y=z)$
Roughly, I proceed as follows...
$(1) \>\>(\forall x)(\forall y)(\exists z)(x \,\circ\,y=z)$ premise
$(2) \>\>(\exists z)(x \,\circ\,y=z)$ by US
$(3) \>\>x \,\circ\,y= \alpha_{xy}\>$ by ES
$(4) \>\>x \,\circ\,y=\alpha_{xy} \circ e\>$ by axiom 2
$(5) \>\>x \,\circ\,y=\alpha_{xy} \circ (y \circ y^{-1})\>$ by axiom 3
$(6) \>\>x \,\circ\,y=\alpha_{xy} \circ (y^{-1} \circ y)\>$ by theorem 4
$(7) \>\>x \,\circ\,y=(\alpha_{xy} \circ y^{-1}) \circ y\>$ by axiom 1
$(8) \>\>x =\alpha_{xy} \circ y^{-1}\>$ by theorem 1
$(9) \>\>(\exists z)(x =z \circ y^{-1})\>$ by EG
Now here I'm stuck. Intuitively, I think a valid deduction would obtained from applying universal generalisation on $y^{-1}$ to yield
$(10) \>\>(\forall y)(\exists z)(x =z \circ y)\>$ by UG on $y^{-1}$
because firstly, $y$ doesn't appear anywhere else in formula. Secondly, since y can be anything in the domain, $y^{-1}$ can be anything in the domain as well (unless I'm mistaken). My idea is something like substituting a variable to act as $y^{-1}$ and to universally generalise on that variable.
However, $y^{-1}$ is strictly defined as term rather than a variable, and in no part of the textbook I'm reading does it explain that such a move is valid. The rule for UG I'm given is defined only for variables rather than for terms in general.
Maybe I'm approaching it the wrong way. I would appreciate any hints :)