Integer multiplication is well defined

By hypothesis $a+b^{\mathrm{\prime }}=b+a^{\mathrm{\prime }}$; write $s$ for this common value.

Regrouping and factoring: $(ac+bd)+(a^{\mathrm{\prime }}d+b^{\mathrm{\prime }}c)=c(a+b^{\mathrm{\prime }})+d(b+a^{\mathrm{\prime }})$.

Regrouping and factoring: $(ad+bc)+(a^{\mathrm{\prime }}c+b^{\mathrm{\prime }}d)=d(a+b^{\mathrm{\prime }})+c(b+a^{\mathrm{\prime }})$.

By step 1.1 both right-hand sides equal $cs+ds$, so $(ac+bd)+(a^{\mathrm{\prime }}d+b^{\mathrm{\prime }}c)=(ad+bc)+(a^{\mathrm{\prime }}c+b^{\mathrm{\prime }}d)$.

That equation is precisely the defining relation $(ac+bd,ad+bc)\sim (a^{\mathrm{\prime }}c+b^{\mathrm{\prime }}d,a^{\mathrm{\prime }}d+b^{\mathrm{\prime }}c)$: the product class is unchanged when the first factor's representative changes.

The product formula is symmetric in its two arguments: swapping $(a,b)\leftrightarrow (c,d)$ sends $(ac+bd,ad+bc)$ to $(ca+db,cb+da)$, the same pair. Hence, by the argument of steps 1.1–3.1 applied to the second factor, the product class is also unchanged when $(c,d)$ is replaced by $(c^{\mathrm{\prime }},d^{\mathrm{\prime }})$.

Replacing first $(a,b)$ by $(a^{\mathrm{\prime }},b^{\mathrm{\prime }})$ and then $(c,d)$ by $(c^{\mathrm{\prime }},d^{\mathrm{\prime }})$: $[(a,b)]\cdot [(c,d)]=[(a^{\mathrm{\prime }},b^{\mathrm{\prime }})]\cdot [(c,d)]=[(a^{\mathrm{\prime }},b^{\mathrm{\prime }})]\cdot [(c^{\mathrm{\prime }},d^{\mathrm{\prime }})]$; multiplication is well defined.