Description: Define predicate that determines if some class A is a function.
Definition 10.1 of Quine p. 65. For example, the expression
Fun cos is true once we define cosine ( df-cos ). This is not the
same as defining a specific function's mapping, which is typically done
using the format of cmpt with the maps-to notation (see df-mpt and
df-mpo ). Contrast this predicate with the predicates to determine if
some class is a function with a given domain ( df-fn ), a function
with a given domain and codomain ( df-f ), a one-to-one function
( df-f1 ), an onto function ( df-fo ), or a one-to-one onto function
( df-f1o ). For alternate definitions, see dffun2 , dffun3 ,
dffun4 , dffun5 , dffun6 , dffun7 , dffun8 , and dffun9 .
(Contributed by NM, 1-Aug-1994)