Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 18 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)> | |||||||||
| (2) | Spezialisierung (1) a ← c | ∀b: ∀c: ∀d: <<c=c∧b=d> ⇒ (c·b)=(c·d)> | |||||||||
| (3) | Spezialisierung (2) b ← b | ∀c: ∀d: <<c=c∧b=d> ⇒ (c·b)=(c·d)> | |||||||||
| (4) | Spezialisierung (3) c ← a | ∀d: <<a=a∧b=d> ⇒ (a·b)=(a·d)> | |||||||||
| (5) | Spezialisierung (4) d ← S0 | <<a=a∧b=S0> ⇒ (a·b)=(a·S0)> | |||||||||
| (6) | Theorem 25 | ∀a: (a·S0)=a | |||||||||
| (7) | Spezialisierung (6) a ← a | (a·S0)=a | |||||||||
| (8) | Theorem 1 | ∀a: a=a | |||||||||
| (9) | Spezialisierung (8) a ← a | a=a | |||||||||
| (10) | Hypothese | b=S0 | |||||||||
| (11) | Übernahme (9) | a=a | |||||||||
| (12) | Konjunktion (11), (10) | <a=a∧b=S0> | |||||||||
| (13) | Übernahme (5) | <<a=a∧b=S0> ⇒ (a·b)=(a·S0)> | |||||||||
| (14) | Modus ponens (13), (12) | (a·b)=(a·S0) | |||||||||
| (15) | Übernahme (7) | (a·S0)=a | |||||||||
| (16) | Transitivität (14), (15) | (a·b)=a | |||||||||
| (17) | Konklusion (10), (16) | <b=S0 ⇒ (a·b)=a> | |||||||||
| (18) | Verallgemeinerung (17) nach b | ∀b: <b=S0 ⇒ (a·b)=a> | |||||||||
| (19) | Verallgemeinerung (18) nach a | ∀a: ∀b: <b=S0 ⇒ (a·b)=a> | |||||||||