If $G$ is a group, then $a \ast x = b$ has a unique solution. From "A First Course In Abstract Algebra" by John B. Fraleigh

TheoremIf $G$ is a group with binary operation $\ast$, and if $a$ and $b$ are any elements of $G$, then the linear equations $a \ast x = b$ and $y \ast a = b$ have unique solutions $x$ and $y$ in $G$.
ProofFirst we show the existence of at least one solution by just computing that $a' \ast b$ is a solution of $a \ast x = b$.
Note that
$$\begin{align*}
a \ast (a' \ast b) &= (a \ast a') \ast b & &\text{associative law} \\ 
&= e \ast b & &\text{definition of $a'$} \\ 
&= b & &\text{property of $e$} \\
\end{align*}$$
Thus $x = a' \ast b$ is a solution of $a \ast x = b$. In a similar fashion, $y = b \ast a'$ is a solution of $y \ast a = b$.
To show uniqueness of $y$, we use the standard method of assuming that we have two solutions, $y_1$ and $y_2$, so that $y_1 \ast a = b$ and $y_2 \ast a = b$. Then $y_1 \ast a = y_2 \ast a$, and by Theorem 4.15, $y_1 = y_2$. The uniqueness of $x$ follows similarly. $\blacksquare$

My question.
Why didn't Fraleigh simply solve the equation to show that a solution exists?
I mean: given the equation $a \ast x = b$ we can do as follows
$$\begin{align*}a \ast x &= b \\
a' \ast (a \ast x) &= a' \ast b \\
(a' \ast a) \ast x &= a' \ast b \\
e \ast x &= a' \ast b \\
x &= a' \ast b\end{align*}$$ and this shows two things: that a solution exists and also that the solution is unique.
Is it a matter of style or in this context my way is wrong?
 A: The difference between "a sequence of equations" and a proof are: clearly expressed logical relations between steps; and clearly expressed justification of each step.
Regarding your comment in reponse to @MatthewTowers, you may have "simply used the properties of operation $*$ in a group", but you did not justify your use of those properties, nor did you explain the logical relations amongst your equations.
If you include those justifications and implications, then your list of equations can be converted into a true proof of uniqueness, something like this (which I did by simply cutting and pasting your align* environment and adding some stuff):
$$\begin{align*}
a \ast x &= b \\
\implies a' \ast (a \ast x) &= a' \ast b \quad\text{(well-definedness of $(*)$)} \\
\iff (a' \ast a) \ast x &= a' \ast b \quad\text{(associative law applied on the LHS of the equation)}\\
\iff e \ast x &= a' \ast b \quad\text{(inverse law applied on the LHS of the equation)} \\
\iff x &= a' \ast b \quad\text{(identity law applied on the LHS of the equation)}
\end{align*}
$$
and therefore, following all the implication arrows forwards, we have $a*x=b \implies x = a'*b$, which proves uniqueness.
But, has existence been proved??!?
Look carefully at the implications that I have written out. The first one is only $\implies$; the remainder are $\iff$. In each $\iff$ step, the group law I am applying allows me to rewrite one side of the equation by substitution, leaving the other side unchanged. But the first implication is different: well-definedness of $(*)$ gives only the forward direction of implication $\implies$.
Notice that if the converse of the first implication is true then you can follow all of the implication arrows backwards to prove existence.
So, is the converse of the first implication true?
Yes, of course it is, and one can prove it like this:
\begin{align*}
a' * (a * x) &= a' * b \\
\implies a * (a' * (a * x)) &= a * (a' * b) \quad\text{(well-definedness of $(*)$)}\\
\end{align*}
and so on applying the associative law and inverse law and identity law...
However, that leads to a rather gloppy proof of existence. Fraleigh's proof of existence is much shorter and better.
A: I'll type some of the things that have been said in the comments here because it can be helpful to have them in one place.
As Matthew says: we can't just have a list of equations, we need to be precise about the relation between one equation and the rest. If, like here, nothing is written about how the equations are related some readers will assume that you mean that each line follows naturally from the previous one, while some others will assume that each line follows naturally from the previous one AND MOREOVER that conversely the previous one follows from the current one. But these are two very different things. So we better are clear about which one we mean.
Now suppose that we go with only the first interpretation and you would have annotated your solution as follows:
Suppose that for some $x$ we have:
$$\begin{align*}a \ast x &= b \textrm{, then it follows that} \\
a' \ast (a \ast x) &= a' \ast b \textrm{, so that}\\
(a' \ast a) \ast x &= a' \ast b \textrm{, and hence}\\
e \ast x &= a' \ast b \textrm{, from which it follows that}\\
x &= a' \ast b\end{align*}$$
Now what does this prove? Obviously it shows that IF such and $x$ exist, THEN it must be equal to $a' \ast b$. What it doesn't prove is THAT such an $x$ exist, so you need to type a separate proof of that fact.
Of course, giving such a proof is easy: since we know that IF $x$ exist it must be equal to $a' \ast b$, all we need to do is check that $x = a' \ast b$ does indeed 'do the job'.
AND in a sense you are right that you already typed such a proof: it is just your sequence of equations, but now with the silent assumption that each equation follows from the one below it, rather than the one above it. In annotated form:
$$\begin{align*}
\textrm{define } x &= a' \ast b \textrm{, then clearly} \\
e \ast x &= a' \ast b \textrm{, from which it follows that} \\
(a' \ast a) \ast x &= a' \ast b \textrm{, and hence} \\
a' \ast (a \ast x) &= a' \ast b \textrm{, so that clearly obviously trivially} \\
a \ast x &= b \\
\end{align*}$$
showing that this $x$ is a solution to the desired equation.
In summary: your sequence of statements does indeed show both things (existence and uniqueness) but the distinction is still very much 'there': you get uniqueness by reading from top to bottom and existence by reading from bottom to top.
In this context it is not clear that each step can be taken in both directions just because you typed them above each other, so at least you should make that more explicit.
I hope this answers your question. Apart from that there is a second issue with your proof, also pointed out by Matthew:
I type 'clearly obviously trivially' in the last proof step above because this step (and only this step) is in fact not clear, obvious and trivial at all. In fact it is valid in groups but not, e.g. in $\mathbb{R}$ so adding some additional reasoning why this step holds here is highly desired.
(E.g. we could add some extra lines where we first multiply both sides of the equation by $a$, then simplify the resulting $a \ast a'$ to $e$ and finally removing the $e$'s. But these extra lines are only needed for existence and not for uniqueness, further illustrating the point that in fact there is a difference between the two even in your approach.)
