The proof of the proposition $(\forall a)[a \in \mathbb{F} \rightarrow -(-a) \in \mathbb{F}]$ is given on page 6 of the following link. https://www.math.ucdavis.edu/~emsilvia/math127/chapter1.pdf
We have that $e$ denotes the additive identity and (A2) is the field axiom for commutativity of elements in a field. That is, (A2) is the axiom $$(\forall x)(\forall y)[x,y \in \mathbb{F} \rightarrow x + y = y + x]$$ And (A4) is the axiom $$(\forall a)[a \in \mathbb{F} \rightarrow (\exists (-a))(-a \in \mathbb{F} \rightarrow (-a) + a = a + (-a) = e)]$$ So, (A4) is the additive inverse property for elements in a field.
Lemma: The additive inverse of an element of a field is unique.
Proposition:
$(\forall a)[a \in \mathbb{F} \rightarrow -(-a) \in \mathbb{F}]$
proof.
Suppose that $a \in \mathbb{F}$. By the additive inverse property, $-a \in \mathbb{F}$ and $-(-a) \in \mathbb{F}$ is the additive inverse of $-a$; i.e $$-(-a) + (-a) = e$$ Since $-a$ is the additive inverse of $a$, $$(-a) + a = a + (-a) = e$$ From the uniqueness of additive inverses, we conclude that $-(-a) = a$.
In the given proof, is axiom (A2) implicitly used to show that $-(-a) + (-a) = e$? I thought that we would have to show that $-(-a) + (-a) = (-a) + (-(-a)) = e$, by definition.
Yes, commutativity of addition is used implicitly to conclude that since $-(-a)+(-a)=e$, then also $-a+\big(-(-a)\big)=e$.
The last sentence contains even more implicit argumentation. We know that $$a+(-a)=(-a)+a=e\;,$$ so we know that $-a$ is the additive inverse of $a$, but the same equalities show that $a$ is the additive inverse of $-a$. Uniqueness of that inverse then tells us that the only solution to the equation(s) $$x+(-a)=e=-a+x\tag{1}$$ is $x=a$. And since we know that $-(-a)$ is a solution to $(1)$, we conclude that $-(-a)=a$.