Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (2) | Spezialisierung (1) a ← Se | ∀b: (Se·Sb)=((Se·b)+Se) | |||||||||
| (3) | Spezialisierung (2) b ← f | (Se·Sf)=((Se·f)+Se) | |||||||||
| (4) | Axiom 3 | ∀a: ∀b: (a+Sb)=S(a+b) | |||||||||
| (5) | Spezialisierung (4) a ← (Se·f) | ∀b: ((Se·f)+Sb)=S((Se·f)+b) | |||||||||
| (6) | Spezialisierung (5) b ← e | ((Se·f)+Se)=S((Se·f)+e) | |||||||||
| (7) | Transitivität (3), (6) | (Se·Sf)=S((Se·f)+e) | |||||||||
| (8) | Symmetrie (7) | S((Se·f)+e)=(Se·Sf) | |||||||||
| (9) | Theorem 1 | ∀a: a=a | |||||||||
| (10) | Spezialisierung (9) a ← a | a=a | |||||||||
| (11) | Theorem 18 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)> | |||||||||
| (12) | Spezialisierung (11) a ← c | ∀b: ∀c: ∀d: <<c=c∧b=d> ⇒ (c·b)=(c·d)> | |||||||||
| (13) | Spezialisierung (12) b ← S((Se·f)+e) | ∀c: ∀d: <<c=c∧S((Se·f)+e)=d> ⇒ (c·S((Se·f)+e))=(c·d)> | |||||||||
| (14) | Spezialisierung (13) c ← a | ∀d: <<a=a∧S((Se·f)+e)=d> ⇒ (a·S((Se·f)+e))=(a·d)> | |||||||||
| (15) | Spezialisierung (14) d ← (Se·Sf) | <<a=a∧S((Se·f)+e)=(Se·Sf)> ⇒ (a·S((Se·f)+e))=(a·(Se·Sf))> | |||||||||
| (16) | Konjunktion (10), (8) | <a=a∧S((Se·f)+e)=(Se·Sf)> | |||||||||
| (17) | Modus ponens (15), (16) | (a·S((Se·f)+e))=(a·(Se·Sf)) | |||||||||
| (18) | Hypothese | (a·(Se·Sf))=c | |||||||||
| (19) | Übernahme (17) | (a·S((Se·f)+e))=(a·(Se·Sf)) | |||||||||
| (20) | Transitivität (19), (18) | (a·S((Se·f)+e))=c | |||||||||
| (21) | Konklusion (18), (20) | <(a·(Se·Sf))=c ⇒ (a·S((Se·f)+e))=c> | |||||||||
| (22) | Kontraposition (21) | <¬(a·S((Se·f)+e))=c ⇒ ¬(a·(Se·Sf))=c> | |||||||||
| (23) | Hypothese | ∀d: ¬(a·Sd)=c | |||||||||
| (24) | Spezialisierung (23) d ← ((Se·f)+e) | ¬(a·S((Se·f)+e))=c | |||||||||
| (25) | Übernahme (22) | <¬(a·S((Se·f)+e))=c ⇒ ¬(a·(Se·Sf))=c> | |||||||||
| (26) | Modus ponens (25), (24) | ¬(a·(Se·Sf))=c | |||||||||
| (27) | Verallgemeinerung (26) nach f | ∀f: ¬(a·(Se·Sf))=c | |||||||||
| (28) | Verallgemeinerung (27) nach e | ∀e: ∀f: ¬(a·(Se·Sf))=c | |||||||||
| (29) | Konklusion (23), (28) | <∀d: ¬(a·Sd)=c ⇒ ∀e: ∀f: ¬(a·(Se·Sf))=c> | |||||||||
| (30) | Kontraposition (29) | <¬∀e: ∀f: ¬(a·(Se·Sf))=c ⇒ ¬∀d: ¬(a·Sd)=c> | |||||||||