Description: Alternate definition of the function relation predicate, cf.
dfdisjALTV3 . Reproduction of dffun2 . For the X axis and the
Y axis you can convert the right side to ( A. x1 A. y1
A. y2 ( ( x1 f y1 /\ x1 f y2 ) -> y1 = y2
) /\ Rel F ) . (Contributed by NM, 29-Dec-1996)