Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (2) | Spezialisierung (1) a ← a | ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (3) | Spezialisierung (2) b ← 0 | (a·S0)=((a·0)+a) | |||||||||
| (4) | Axiom 4 | ∀a: (a·0)=0 | |||||||||
| (5) | Spezialisierung (4) a ← a | (a·0)=0 | |||||||||
| (6) | Theorem 9 | ∀a: ∀b: ∀c: <a=b ⇒ (a+c)=(b+c)> | |||||||||
| (7) | Spezialisierung (6) a ← (a·0) | ∀b: ∀c: <(a·0)=b ⇒ ((a·0)+c)=(b+c)> | |||||||||
| (8) | Spezialisierung (7) b ← 0 | ∀c: <(a·0)=0 ⇒ ((a·0)+c)=(0+c)> | |||||||||
| (9) | Spezialisierung (8) c ← a | <(a·0)=0 ⇒ ((a·0)+a)=(0+a)> | |||||||||
| (10) | Modus ponens (9), (5) | ((a·0)+a)=(0+a) | |||||||||
| (11) | Transitivität (3), (10) | (a·S0)=(0+a) | |||||||||
| (12) | Theorem 5 | ∀a: (0+a)=a | |||||||||
| (13) | Spezialisierung (12) a ← a | (0+a)=a | |||||||||
| (14) | Transitivität (11), (13) | (a·S0)=a | |||||||||
| (15) | Verallgemeinerung (14) nach a | ∀a: (a·S0)=a | |||||||||
Interpretation:
1 ist multiplikativ rechtsneutral