ZF* Minus Extensionality

The attached file presents a full proof of ZF* minus Extensionality interpreting full ZF.

This sketch of this proof had also been posted to MathOverflow at:

Can ZF be interpreted in a theory axiomatized by a version of Replacement and Infinity

Equivalents of Replacement under removal of Extensionality

Is this kind of Predication preserved under co-extensionality