Opposite categories and contravariant functors

WWW:http://mizar.org/JFM/Vol3/oppcat_1.html The articles [6], [4], [7], [8], [1], [2], [5], and [3] provide the notation and terminology for this paper. In this paper B, C, D are categories. Let X, Y, Z be non empty sets and let f be a partial function from [:X, Y:] to Z. Then � f is a partial function from [:Y, X:] to Z. Next we state the propositio