Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 4 | ∀a: (a·0)=0 | |||||||||
| (2) | Spezialisierung (1) a ← Sa | (Sa·0)=0 | |||||||||
| (3) | Theorem 28 | ∀a: ∀b: ∀c: <(Sc·a)=(Sc·b) ⇒ a=b> | |||||||||
| (4) | Spezialisierung (3) a ← 0 | ∀b: ∀c: <(Sc·0)=(Sc·b) ⇒ 0=b> | |||||||||
| (5) | Spezialisierung (4) b ← b | ∀c: <(Sc·0)=(Sc·b) ⇒ 0=b> | |||||||||
| (6) | Spezialisierung (5) c ← a | <(Sa·0)=(Sa·b) ⇒ 0=b> | |||||||||
| (7) | Hypothese | (Sa·b)=0 | |||||||||
| (8) | Symmetrie (7) | 0=(Sa·b) | |||||||||
| (9) | Übernahme (2) | (Sa·0)=0 | |||||||||
| (10) | Transitivität (9), (8) | (Sa·0)=(Sa·b) | |||||||||
| (11) | Übernahme (6) | <(Sa·0)=(Sa·b) ⇒ 0=b> | |||||||||
| (12) | Modus ponens (11), (10) | 0=b | |||||||||
| (13) | Symmetrie (12) | b=0 | |||||||||
| (14) | Konklusion (7), (13) | <(Sa·b)=0 ⇒ b=0> | |||||||||
| (15) | Verallgemeinerung (14) nach b | ∀b: <(Sa·b)=0 ⇒ b=0> | |||||||||
| (16) | Verallgemeinerung (15) nach a | ∀a: ∀b: <(Sa·b)=0 ⇒ b=0> | |||||||||