The question is in the title. The definition of $+:\mathbb{N} \times \mathbb{N} \to \mathbb{N}$ is given as follows:
$$\forall m,n \in \mathbb{N}: [n+1 := n'] \land [n+m' := (n+m)']$$
where $n'$ refers to the successor of $n$.
Proof Attempt:
We note that this is a relation and in order to prove that it is a binary operation, we need to show that it is a function. Thus, it has to be totally-defined and well-defined. We prove the former first and then, prove the latter.
Let $m \in \mathbb{N}$ be fixed. Define the following set:
$$S = \{n \in \mathbb{N} : (\exists k \in \mathbb{N}: m+n = k)\}$$
Clearly, $1 \in S$ because $m+1 = m'$ so we have our desired $k$.
Now, suppose that $n \in S$. There exists a $k \in \mathbb{N}$ so that $m+n = k$. Then, $m+n' = (m+n)' = k'$. Since $k' \in \mathbb{N}$, we have the desired image of $(m,n')$ under $+$. So, $n' \in S$. By the Axiom of Induction, $S = \mathbb{N}$. This proves that $+$ is totally-defined.
Now, we prove that $+$ is well-defined. Let $m \in \mathbb{N}$ be fixed. Define the following set:
$$S = \{n \in \mathbb{N}: [(m+n = k_1) \land (m+n = k_2) \implies (k_1 = k_2)]\}$$
Clearly, $1 \in S$ because $m+1 = m'$ by definition of $+$. That sum is well-defined.
Now, suppose that $n \in S$. Then, the sum $m+n = k$ is well-defined. So, $m+n' = (m+n)' = k'$ due to the fact that $m+n$ is well-defined. Hence, $n' \in S$. By the Axiom of Induction, it follows that $S = \mathbb{N}$. This proves that $+$ is well-defined.
Since $+$ is both well-defined and totally-defined, it follows that it is a function and a binary operation on $\mathbb{N}$.
Does the proof above work? If it doesn't, why? How can I fix it?
The first part is fine. In the second part your induction doesn’t really get off the ground: you know that $m+1=m'$ by definition, but that doesn’t in itself rule out the possibility that $m+1$ is also equal to some other $k\in\Bbb N$.
Suppose that $m+1=k$. Then either $k=1$, or $k=\ell'$ for some $\ell\in\Bbb N$. If $k=1$, then $1=m+1=m'$, which is impossible, so $k=\ell'$, and therefore $\ell'=k=m+1=m'$, $\ell=m$, and $k=m'$, as desired.
The induction step also needs a bit of expansion. We assume that $m+n=k$ is well-defined. We know that $m+n'=(m+n)'=k'$, but we have to show that this is the only value of $m+n'$, so suppose that $m+n'=\ell$. Then $\ell=m+n'=(m+n)'=k'$. Again, either $\ell=1$, or $\ell=i'$ for some $i\in\Bbb N$. Clearly $\ell\ne 1$, since $1$ is not a successor, so $k'=\ell=i'$, $i=k$, and $\ell=k'$, as desired.