General Associative Law for Ordinal Sum/Proof 2
Jump to navigation
Jump to search
Theorem
Let $x$ be a finite ordinal.
Let $\sequence {a_i}$ be a sequence of ordinals.
Then:
- $\ds \sum_{i \mathop = 1}^{x + 1} a_i = a_1 + \sum_{i \mathop = 1}^x a_{i + 1}$
Proof
From Ordinal Addition is Associative we have that:
- $\forall a, b, c \in \On: a + \paren {b + c} = \paren {a + b} + c$
The result follows directly from the General Associativity Theorem.
$\blacksquare$