Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 17 | ∀a: ∀b: ∀c: <a=b ⇒ (a·c)=(b·c)> | |||||||||
| (2) | Spezialisierung (1) a ← a | ∀b: ∀c: <a=b ⇒ (a·c)=(b·c)> | |||||||||
| (3) | Spezialisierung (2) b ← d | ∀c: <a=d ⇒ (a·c)=(d·c)> | |||||||||
| (4) | Spezialisierung (3) c ← b | <a=d ⇒ (a·b)=(d·b)> | |||||||||
| (5) | Verallgemeinerung (4) nach d | ∀d: <a=d ⇒ (a·b)=(d·b)> | |||||||||
| (6) | Spezialisierung (5) d ← c | <a=c ⇒ (a·b)=(c·b)> | |||||||||
| (7) | Spezialisierung (3) c ← c | <a=d ⇒ (a·c)=(d·c)> | |||||||||
| (8) | Verallgemeinerung (7) nach a | ∀a: <a=d ⇒ (a·c)=(d·c)> | |||||||||
| (9) | Spezialisierung (8) a ← b | <b=d ⇒ (b·c)=(d·c)> | |||||||||
| (10) | Theorem 16 | ∀a: ∀b: (a·b)=(b·a) | |||||||||
| (11) | Spezialisierung (10) a ← c | ∀b: (c·b)=(b·c) | |||||||||
| (12) | Spezialisierung (11) b ← b | (c·b)=(b·c) | |||||||||
| (13) | Spezialisierung (11) b ← d | (c·d)=(d·c) | |||||||||
| (14) | Symmetrie (13) | (d·c)=(c·d) | |||||||||
| (15) | Hypothese | <a=c∧b=d> | |||||||||
| (16) | Abtrennung I (15) | a=c | |||||||||
| (17) | Abtrennung II (15) | b=d | |||||||||
| (18) | Übernahme (6) | <a=c ⇒ (a·b)=(c·b)> | |||||||||
| (19) | Übernahme (9) | <b=d ⇒ (b·c)=(d·c)> | |||||||||
| (20) | Modus ponens (18), (16) | (a·b)=(c·b) | |||||||||
| (21) | Modus ponens (19), (17) | (b·c)=(d·c) | |||||||||
| (22) | Übernahme (12) | (c·b)=(b·c) | |||||||||
| (23) | Transitivität (20), (22) | (a·b)=(b·c) | |||||||||
| (24) | Transitivität (23), (21) | (a·b)=(d·c) | |||||||||
| (25) | Übernahme (14) | (d·c)=(c·d) | |||||||||
| (26) | Transitivität (24), (25) | (a·b)=(c·d) | |||||||||
| (27) | Konklusion (15), (26) | <<a=c∧b=d> ⇒ (a·b)=(c·d)> | |||||||||
| (28) | Verallgemeinerung (27) nach d | ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)> | |||||||||
| (29) | Verallgemeinerung (28) nach c | ∀c: ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)> | |||||||||
| (30) | Verallgemeinerung (29) nach b | ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)> | |||||||||
| (31) | Verallgemeinerung (30) nach a | ∀a: ∀b: ∀c: ∀d: <<a=c∧b=d> ⇒ (a·b)=(c·d)> | |||||||||
Interpretation:
Das Produkt ist eine Funktion in beiden Variablen