Bizonyítás
Az f függvény definíciója alapján egyrészt:
\begin{aligned}
f(a)&=[(a;0)] \\
f(b)&=[(b;0)] \\
f(a+b)&=[(a+b;0)] \\
\end{aligned}
Másrészt a 13.13. Definícióban bevezetett \oplus művelet definíciója miatt igaz az alábbi:
f(a)\oplus f(b)=\underbrace{[(a;0)]}_{=f(a)}\oplus \underbrace{[(b;0)]}_{=f(b)} = [(a+b;0)]
Az eredményül kapott két kifejezés megegyezik, tehát valóban:
f(a+b)=f(a)\oplus f(b)
Azt kell még belátnunk, hogy az f függvény valóban injektív, azaz különböző elemek képe különböző lesz. Tegyük fel indirekt, hogy nem ez a helyzet, azaz léteznek olyan n és m elemek \N_1-ben, amelyek esetén n\neq m, ugyanakkor
f(n)=f(m)
Ez az f függvény definíciója alapján azt jelentené, hogy
[(n;0)]=[(m;0)]
Ez viszont a 13.10. Tétel alapján azt jelentené, hogy n=m, ami ellentmond az indirekt feltételünknek.
∎