Es gelten die allgemeinen Vorbemerkungen.
| (1) | Axiom 4 | ∀a: (a·0)=0 | |||||||||
| (2) | Spezialisierung (1) a ← a | (a·0)=0 | |||||||||
| (3) | Spezialisierung (1) a ← b | (b·0)=0 | |||||||||
| (4) | Symmetrie (3) | 0=(b·0) | |||||||||
| (5) | Transitivität (2), (4) | (a·0)=(b·0) | |||||||||
| (6) | Hypothese | a=b | |||||||||
| (7) | Übernahme (5) | (a·0)=(b·0) | |||||||||
| (8) | Konklusion (6), (7) | <a=b ⇒ (a·0)=(b·0)> | |||||||||
| (9) | Axiom 5 | ∀a: ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (10) | Spezialisierung (9) a ← a | ∀b: (a·Sb)=((a·b)+a) | |||||||||
| (11) | Spezialisierung (10) b ← c | (a·Sc)=((a·c)+a) | |||||||||
| (12) | Verallgemeinerung (11) nach a | ∀a: (a·Sc)=((a·c)+a) | |||||||||
| (13) | Spezialisierung (12) a ← b | (b·Sc)=((b·c)+b) | |||||||||
| (14) | Symmetrie (13) | ((b·c)+b)=(b·Sc) | |||||||||
| (15) | Theorem 10 | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a+b)=(c+d)> | |||||||||
| (16) | Spezialisierung (15) a ← e | ∀b: ∀c: ∀d: <<e=c∧b=d> ⇒ (e+b)=(c+d)> | |||||||||
| (17) | Spezialisierung (16) b ← a | ∀c: ∀d: <<e=c∧a=d> ⇒ (e+a)=(c+d)> | |||||||||
| (18) | Spezialisierung (17) c ← (b·c) | ∀d: <<e=(b·c)∧a=d> ⇒ (e+a)=((b·c)+d)> | |||||||||
| (19) | Spezialisierung (18) d ← b | <<e=(b·c)∧a=b> ⇒ (e+a)=((b·c)+b)> | |||||||||
| (20) | Verallgemeinerung (19) nach e | ∀e: <<e=(b·c)∧a=b> ⇒ (e+a)=((b·c)+b)> | |||||||||
| (21) | Spezialisierung (20) e ← (a·c) | <<(a·c)=(b·c)∧a=b> ⇒ ((a·c)+a)=((b·c)+b)> | |||||||||
| (22) | Hypothese | <a=b ⇒ (a·c)=(b·c)> | |||||||||
| (23) | Hypothese | a=b | |||||||||
| (24) | Übernahme (21) | <<(a·c)=(b·c)∧a=b> ⇒ ((a·c)+a)=((b·c)+b)> | |||||||||
| (25) | Übernahme (22) | <a=b ⇒ (a·c)=(b·c)> | |||||||||
| (26) | Modus ponens (25), (23) | (a·c)=(b·c) | |||||||||
| (27) | Konjunktion (26), (23) | <(a·c)=(b·c)∧a=b> | |||||||||
| (28) | Modus ponens (24), (27) | ((a·c)+a)=((b·c)+b) | |||||||||
| (29) | Übernahme (11) | (a·Sc)=((a·c)+a) | |||||||||
| (30) | Transitivität (29), (28) | (a·Sc)=((b·c)+b) | |||||||||
| (31) | Übernahme (14) | ((b·c)+b)=(b·Sc) | |||||||||
| (32) | Transitivität (30), (31) | (a·Sc)=(b·Sc) | |||||||||
| (33) | Konklusion (23), (32) | <a=b ⇒ (a·Sc)=(b·Sc)> | |||||||||
| (34) | Konklusion (22), (33) | <<a=b ⇒ (a·c)=(b·c)> ⇒ <a=b ⇒ (a·Sc)=(b·Sc)>> | |||||||||
| (35) | Verallgemeinerung (34) nach c | ∀c: <<a=b ⇒ (a·c)=(b·c)> ⇒ <a=b ⇒ (a·Sc)=(b·Sc)>> | |||||||||
| (36) | Induktion (8), (35) | ∀c: <a=b ⇒ (a·c)=(b·c)> | |||||||||
| (37) | Verallgemeinerung (36) nach b | ∀b: ∀c: <a=b ⇒ (a·c)=(b·c)> | |||||||||
| (38) | Verallgemeinerung (37) nach a | ∀a: ∀b: ∀c: <a=b ⇒ (a·c)=(b·c)> | |||||||||
Interpretation:
Multipliaktion ist eine Funktion im ersten Faktor