Let be a Function Class defined everywhere. Then there is a function class defined everywhere such that: Also is unique. Note is the set which is a set by Axiom of Replacement Proof Uniqueness by Principle of Epsilon-Induction We say is an attempt if is a function is transitive and Note that makes sense as is transitive. Now use induction to show two attempts agree on intersection of their domains Another induction shows every set is in domain for some Then is defined by