Es gelten die allgemeinen Vorbemerkungen.
| (1) | Theorem 9 | ∀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 8 | ∀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) | Übernahme (6) | <a=c ⇒ (a+b)=(c+b)> | |||||||||
| (17) | Abtrennung I (15) | a=c | |||||||||
| (18) | Modus ponens (16), (17) | (a+b)=(c+b) | |||||||||
| (19) | Übernahme (9) | <b=d ⇒ (b+c)=(d+c)> | |||||||||
| (20) | Abtrennung II (15) | b=d | |||||||||
| (21) | Modus ponens (19), (20) | (b+c)=(d+c) | |||||||||
| (22) | Übernahme (12) | (c+b)=(b+c) | |||||||||
| (23) | Transitivität (18), (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:
Addition ist eine Funktion in beiden Summanden