Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 2 | ∀a: (a+0)=a | |||||||||
| (2) | Spezialisierung (1) a ← Sa | (Sa+0)=Sa | |||||||||
| (3) | Spezialisierung (1) a ← a | (a+0)=a | |||||||||
| (4) | Symmetrie (3) | a=(a+0) | |||||||||
| (5) | S hinzufügen (4) | Sa=S(a+0) | |||||||||
| (6) | Transitivität (2), (5) | (Sa+0)=S(a+0) | |||||||||
| (7) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (8) | Spezialisierung (7) a ← a | ∀b: (a+Sb)=S(a+b) | |||||||||
| (9) | Spezialisierung (8) b ← b | (a+Sb)=S(a+b) | |||||||||
| (10) | Spezialisierung (7) a ← Sa | ∀b: (Sa+Sb)=S(Sa+b) | |||||||||
| (11) | Spezialisierung (10) b ← b | (Sa+Sb)=S(Sa+b) | |||||||||
| (12) | Hypothese | (Sa+b)=S(a+b) | |||||||||
| (13) | Übernahme (11) | (Sa+Sb)=S(Sa+b) | |||||||||
| (14) | S hinzufügen (12) | S(Sa+b)=SS(a+b) | |||||||||
| (15) | Übernahme (9) | (a+Sb)=S(a+b) | |||||||||
| (16) | S hinzufügen (15) | S(a+Sb)=SS(a+b) | |||||||||
| (17) | Symmetrie (16) | SS(a+b)=S(a+Sb) | |||||||||
| (18) | Transitivität (13), (14) | (Sa+Sb)=SS(a+b) | |||||||||
| (19) | Transitivität (18), (17) | (Sa+Sb)=S(a+Sb) | |||||||||
| (20) | Konklusion (12), (19) | <(Sa+b)=S(a+b) ⇒ (Sa+Sb)=S(a+Sb)> | |||||||||
| (21) | Verallgemeinerung (20) nach b | ∀b: <(Sa+b)=S(a+b) ⇒ (Sa+Sb)=S(a+Sb)> | |||||||||
| (22) | Induktion (6), (21) | ∀b: (Sa+b)=S(a+b) | |||||||||
| (23) | Verallgemeinerung (22) nach a | ∀a: ∀b: (Sa+b)=S(a+b) | |||||||||