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