I am reading the proof of addition of numbers.
In the proof author first shows uniqueness of $x+y$ and then the existence of plus operation with the above listed properties.
The second proof is as shown below.
In this the induction on x is applied.
My question is that for $x=1,\;1+y=y'$ is defined or assumed. and for arbitrary $x \in \mathfrak R,\;x'+y=(x+y)'$ is defined to complete the proof.
I have read the answer to the following two posts-
But I don't understand the answer for the exact reason how the author basically suppose $1+y=y'$ and $x'+y=(x+y)'$ for $x=1$ and $x\in\mathfrak R$.
Does the author use the uniqueness of "plus" to assume the above thing or there is something different reasoning?
Please explain what is the justification to the supposition use in the proof?


The poof is a little bit "idiosyncratic" but it amounts to showing that the definition of "+" is a "good" definition of a binary operation.
In formula, the author proves that:
where obviously the domain of variables is the collection of natural numbers.
The author starts with the uniqueness part (A).
Then he proves the existence part (B). How to do this by induction ?
Let $\mathfrak M = \{ x \in \mathbb N \mid \exists z (x+y=z), \text { for every } y \}$.
It is by definition a subset of $\mathbb N$. In order to achieve the goal, we have to show that $\mathbb N \subseteq \mathfrak M$.
I) Let's start with $x=1$ and prove that $\exists z (1+y=z)$, for every $y$.
For $y=1$ we have: $1+y=1+1=1'$, using the part $x+1=x'$ of the definition of sum.
By Ax.2, the successor of $1$ exists and thus we have proved that $\exists z (1+1=z)$.
Now assume that $1+y$ exists and consider $y'$.
We have: $1+y'= y'+1 ( \text { using properties of equality}) = (y')'$, using again the definition of sum. And this is: $(y+1)'.$
Again we have that: $\exists z (1+y'=z)$.
In conclusion, we have proved that: $\exists z (1+y=z)$, for every $y$.
This concludes the base step: $1 \in \mathfrak M$.
II) Now the inductive step: assume that $x \in \mathfrak M$ and prove that $x' \in \mathfrak M$.
Having done this, we will use Ax.5 to conclude that $\mathfrak M$ contains all the natural numbers and the theorem is proved.
The argument is the same: assume that $\exists z (x+y=z)$, for every $y$, and prove (by induction on $y$) that $\exists z (x'+y=z)$, for every $y$.
We have $x'+1=(x')'=(x+1)'$, using the first part of the definition of sum.
Now assume the existence of $x'+y$ and compute $x'+y'$.
We have: $x'+y'=(x'+y)'$, using the second part of the definition of sum. But $x'+y$ exists, and thus we have that also $x'+y'$ exists, showing that $\exists z (x+y=z)$, for every $y$.