Let and We call a fixed point of if (using notation from The Software Principle)

Theorem

If is total, then has a fixed point.

Proof

Consider the Partial Function

Apply The s-m-n Theorem to find a total function such that:

Now consider such that Note so Let Then

Thus is a fixpoint