Bizonyítás

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

f(a)=[(a;0)]f(b)=[(b;0)]f(ab)=[(ab;0)]\begin{aligned} f(a)&=[(a;0)] \\ f(b)&=[(b;0)] \\ f(ab)&=[(ab;0)] \\ \end{aligned}

Másrészt a 14.3. Definícióban bevezetett \odot művelet definíciója miatt igaz az alábbi:

f(a)f(b)=[(a;0)]=f(a)[(b;0)]=f(b)=[(ab;0)]f(a)\odot f(b)=\underbrace{[(a;0)]}_{=f(a)}\odot \underbrace{[(b;0)]}_{=f(b)} = [(ab;0)]

Az eredményül kapott két kifejezés megegyezik, tehát valóban:

f(ab)=f(a)f(b)f(ab)=f(a)\odot f(b)

Azt, hogy ff injektív, már a 13.14. Tétel bizonyításában beláttuk.