How the following step in the proof of this theorem is justified by group axioms? In my university, we have just did a proof of the following very basic theorem from linear algebra: "Let's have a group $(M,*)$ and $a,b\in M$. Then $x=a^{-1}*b$ is the only solution to the equation $a*x=b$."
I know how to show from the group axioms that $x=a^{-1}*b$ is a solution to the equation $a*x=b$.
However one thing is not clear to me when doing the second part of the proof, namely proving that $x=a^{-1}*b$ is the only solution to this equation. In school, we did the proof of this second part as follows:
"Suppose that $x'$ is also a solution to the equation $a*x=b$ . Therefore, $a*x'=b$. Than I can multiply both sides of the equation by $a^{-1}$ to get $a^{-1}*(a*x')=a^{-1}*b$. Then from association axiom I can move the backets as follows: $(a^{-1}*a)*x'=a^{-1}b$ and from another axiom I get $e*x'=a^{-1}b$ and from neutrality axiom I get $x'=a^{-1}b$."
The only step of this proof which I don't see to be justified by group axioms is the step where I'm basically saying that multiplying both sides of the equation by a same thing doesn't change the equality. It seems to be obvious, but shouldn't be there an axiom for that? Why not?
 A: There is an axiom for that, namely:

$*$ is a binary operation on $G$. 

By definition, a binary operation on $G$ is a function 
$$G \times G \mapsto G
$$
which is denoted
$$(g,h) \mapsto g * h
$$
And since it is a function, it follows that if $(g,h) = (g',h')$ then $g * h = g' * h'$. Equivalently, if $g=g'$ and $h=h'$ then $g*h=g'*h'$.
So, using $g=g'=a^{-1}$, and using $h=a * x'$ and $h' = b$, and knowing by hypothesis that $h=a*x'=b=h'$, it follows that $g * h = g' * h'$, and then by substitution we get
$$a^{-1} * (a * x') = a^{-1} * b
$$
and you know where to go from there.
A: Group theory defines elements, a binary operator, and an identity. It requires certain axioms relating things things together be satisfied. But it does not define equality. "Equality" in group theory equations just means sameness, just like it does for numbers, functions, and in most contexts.
The statement $a * x = b$ just says the group element $a * x$ is the same thing as the group element $b$. Implicit in that statement is that the formula $a * x$ means exactly one specific group element, which depends on the fact that $*$ is a function from a pair of group elements to a group element. The symbol $=$ can also be used for sets of group elements to say those sets are the same.
So if $a*x'=b$, then of course $a^{-1}*(a*x') = a^{-1}*b$ since $a*x'$ is the same thing as $b$. We do need to make sure what we write makes sense in terms of domains of functions, but otherwise this isn't really a property of the $*$ operator. We can just as well conclude $f(a*x') \oplus \varsigma = f(b) \oplus \varsigma$ without knowing anything about $f$, $\oplus$, or $\varsigma$ other than that those expressions make sense for any elements from our group $G$.
In formal proof theory, there is sort of a principle of substitutability, saying that if two formulae are proved to be equal, then substituting each of them for a free variable in any other formula is a valid proof step. But this is typically considered more of a principle at the level of the logic underlying mathematics, like "if $p$ and $p \rightarrow q$ are previous results in a formal proof, then $q$ is a valid next step", and is not usually included with the mathematical axioms forming the starting points for proofs.
However, this is not a universal meaning of "$=$" in mathematics. The symbol $=$ usually means just sameness, but is sometimes used to mean things which aren't really saying that the left side and the right side are the same thing. One example: in some common definition systems, the "equation"
$$ \lim_{x \to a} f(x) = +\infty $$
doesn't claim that either side of the equation alone represents any meaningful value; it only asserts a certain property about the behavior of function $f$ for arguments near a value $a$.
