Zermelo set theory, Mac Lane set theory and set forcing

Over certain transitive models of Z, the usual treatment of forcing goes awry. But the provident closure of any such set is a provident model of Z, over which, as shown in "Provident sets and rudimentary set forcing", forcing works well. In "The Strength of Mac Lane Set Theory" a process is described of passing from a transitive model of Z + Tco to what is here called its lune, which is a larger model of Z + KP.

Theorem: Over a provident model of Z, the two operations of forming lunes and generic extensions commute.

Corresponding results hold for transitive models of Mac Lane set theory + Tco.