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 ← 0 | ∀c: ∀d: <<c=c∧0=d> ⇒ (c·0)=(c·d)> | |||||||||
| (4) | Spezialisierung (3) c ← a | ∀d: <<a=a∧0=d> ⇒ (a·0)=(a·d)> | |||||||||
| (5) | Spezialisierung (4) d ← b | <<a=a∧0=b> ⇒ (a·0)=(a·b)> | |||||||||
| (6) | Theorem 1 | ∀a: a=a | |||||||||
| (7) | Spezialisierung (6) a ← a | a=a | |||||||||
| (8) | Axiom 4 | ∀a: (a·0)=0 | |||||||||
| (9) | Spezialisierung (8) a ← a | (a·0)=0 | |||||||||
| (10) | Hypothese | b=0 | |||||||||
| (11) | Symmetrie (10) | 0=b | |||||||||
| (12) | Übernahme (7) | a=a | |||||||||
| (13) | Konjunktion (12), (11) | <a=a∧0=b> | |||||||||
| (14) | Übernahme (5) | <<a=a∧0=b> ⇒ (a·0)=(a·b)> | |||||||||
| (15) | Modus ponens (14), (13) | (a·0)=(a·b) | |||||||||
| (16) | Symmetrie (15) | (a·b)=(a·0) | |||||||||
| (17) | Übernahme (9) | (a·0)=0 | |||||||||
| (18) | Transitivität (16), (17) | (a·b)=0 | |||||||||
| (19) | Konklusion (10), (18) | <b=0 ⇒ (a·b)=0> | |||||||||
| (20) | Verallgemeinerung (19) nach b | ∀b: <b=0 ⇒ (a·b)=0> | |||||||||
| (21) | Verallgemeinerung (20) nach a | ∀a: ∀b: <b=0 ⇒ (a·b)=0> | |||||||||