ZF: NEW DEFINITION OF PI(A,B) Was Pi(A,B) == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f} Now function(r) == ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y') Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}" This simplifies many proofs, since (a) the top-level definition has fewer bound variables (b) the "total" and "function" properties are separated (c) the awkward EX! quantifier is eliminated. ZF/ZF.thy/function: new definition