Theorem: Infinite Ordinal can be expressed Uniquely as Sum of Limit Ordinal plus Finite Ordinal

Let $x$ be an ordinal.
Suppose $x$ satisfies $\omega \subseteq x$.
Then $x$ has a unique representation as $\paren {y + z}$ where $y$ is a limit ordinal and $z$ is a finite ordinal.

Proof:
Take $K_{II}$ to be the set of all limit ordinals.
Then set $y = \bigcup \set {w \in K_{II}: w \le x}$
The set $\set {w \in K_{II}: w \le x}$ is non-empty because $\omega \subseteq x$.
By Union of Ordinals is Least Upper Bound, $y \in K_{II}$ and $y \le x$.
By Ordinal Subtraction when Possible is Unique, there is a unique $z$ such that $x = \paren {y + z}$
Assume $\omega \le z$.
Then, again by Ordinal Subtraction when Possible is Unique:
:$z = \paren {\omega + w}$
and so:
{{begin-eqn}}
{{eqn | l = x
      | r = \paren {y + \paren {\omega + w} }
      | c = Equality is Transitive
}}
{{eqn | r = \paren {\paren {y + \omega} + w}
      | c = Ordinal Addition is Associative
}}
{{end-eqn}}
But $y + \omega$ is a limit ordinal by Limit Ordinals Preserved Under Ordinal Addition:
:$\O < \omega \implies y < y + \omega$
This contradicts the fact that $y$ is the largest limit ordinal smaller than $x$.
Therefore, $z \in \omega$.
Thus we have proven that such a selection of $y$ and $z$ exists.
Suppose $z$ and $w$ both satisfy:
:$\paren {y + w} = \paren {y + z}$
By Ordinal Addition is Left Cancellable, we have $w = z$.
Thus $z$ is unique.
It remains to prove uniqueness for $y$.
Suppose that $x = \paren {y + u}$ and $x = \paren {w + z}$.
{{WLOG}}, assume further that $y \le w$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | o = \le
      | r = w
      | c =
}}
{{eqn | ll= \leadsto
      | q = \exists n
      | l = w
      | r = \paren {y + n}
      | c = Ordinal Subtraction when Possible is Unique
}}
{{eqn | ll= \leadsto
      | l = \paren {y + u}
      | r = \paren {\paren {y + n} + z}
      | c = Substitutivity of Equality
}}
{{eqn | ll= \leadsto
      | l = \paren {y + u}
      | r = \paren {y + \paren {n + z} }
      | c = Ordinal Addition is Associative
}}
{{eqn | ll= \leadsto
      | l = u
      | r = \paren {n + z}
      | c = Ordinal Addition is Left Cancellable
}}
{{eqn | ll= \leadsto
      | l = \paren {n + z}
      | o = \in
      | r = \omega
      | c = as $u \in \omega$
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \in
      | r = \omega
      | c = Ordinal is Less than Sum
}}
{{eqn | ll= \leadsto
      | l = n
      | o = \notin
      | r = K_{II}
      | c = as $\omega$ is the smallest limit ordinal
}}
{{eqn | ll= \leadsto
      | l = n
      | r = \O
      | c = {{Defof|Limit Ordinal}}
}}
{{eqn | lo= \lor
      | q = \exists m
      | l = n
      | r = m^+
      | c = 
}}
{{end-eqn}}
{{AimForCont}} that $\exists m: n = m^+$.
{{begin-eqn}}
{{eqn | l = n
      | r = m^+
      | c = 
}}
{{eqn | ll= \leadsto
      | l = w
      | r = \paren {y + m^+}
      | c = Definition of $n$
}}
{{eqn | ll= \leadsto
      | l = w
      | r = \paren {y + m}^+
      | c = {{Defof|Ordinal Addition}}
}}
{{eqn | ll= \leadsto
      | l = w
      | o = \notin
      | r = K_{II}
      | c = {{Defof|Limit Ordinal}}
}}
{{end-eqn}}
This is clearly a contradiction.
Hence:
:$n = \O$
and so:
:$w = y$
The result follows.
{{qed}}