Unconventional indeed. But what is defined here is the predicate IsAFcn not
the concept of function nor the operator [ x \in A |-> B ].
Excuse me. No what is defined by IsAFcn is the operator [ x \in A |-> B ] not
IsAFcn. I had missed the equality.
But unconventional anyway.
--
FL