Bizonyítás

Az ff függvény definíciója alapján egyrészt:

f(a)=[(a;0)]f(b)=[(b;0)]f(a+b)=[(a+b;0)]\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)f(b)=[(a;0)]=f(a)[(b;0)]=f(b)=[(a+b;0)]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)f(b)f(a+b)=f(a)\oplus f(b)

Azt kell még belátnunk, hogy az ff 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 nn és mm elemek N1\N_1-ben, amelyek esetén nmn\neq m, ugyanakkor

f(n)=f(m)f(n)=f(m)

Ez az ff függvény definíciója alapján azt jelentené, hogy

[(n;0)]=[(m;0)][(n;0)]=[(m;0)]

Ez viszont a 13.10. Tétel alapján azt jelentené, hogy n=mn=m, ami ellentmond az indirekt feltételünknek.