Define decreasing sequence in .
Let .
If is a limit ordinal, the fact that is -closed gives us for .
Suppose now that is defined and .
Since , we find such that
Thus set .
This whole definition happens in (doesn’t use )
and so and .
Note that function is a function in .
By -closure, find for all .
But then
which cannot be because (because ).
Corollary
This is a strong preservation theorem:
Forcing with can never add a new function .
So must remain the same.