Definition by recursion

Let be a Well-ordered set and be an arbitrary set.
Then for any Function
there is unique such that

where is the Initial Segment.

Theorem

Say is an attempt if is a function
where the domain of is an Initial Segment of and

(Note that )

WTS that there is a unique attempt whose domain is

We first show that if are attempts, then for all by Proof by Induction.

Fix
Assume for all (induction hypothesis)
(Note that is an initial segment of )
We have

To complete the proof of existence, we let

Now just check that this is a Function and check that is an attempt.
To find the domain of :
If then for some
So there is no attempt defined at
but we know how to do one step extension so this is untrue