Let be a Transitive Model of and with infinite. Let 𝟙 with be a Finite Function Forcing. Suppose is a -Generic Filter over . Then is a surjection from to and . Moreover and: where is the Model Extension of by . Proof First note that 𝟙. As is a Filter, it follows that is a function. Let and be as defined in Finite Function Forcing. Then and , so is both a -Generic Filter and a -Generic Filter. We conclude that and, as is infinite, . Thus is a surjective function . Suppose that and let be as in Finite Function Forcing. Then so is an -Generic Filter. But then is a contradiction. We also know that Model Extension and also . Thus by the Union axiom, and proof of surjectivity can be done in as in Finite Function Forcing.