-functions such that, given any
-function, it is formally equivalent to some function of the type in question."
If this axiom is assumed, we use functions of this type in defining our associated extensional function. Statements about all
-classes (i.e. all classes defined by
-functions) can be reduced to statements about all
-functions of the type