It is easy enough to prove in set theory, but it seems counter-intuitive to me that an empty set could be the domain of a function. Is there any literature requiring that functions have non-empty domains?
I mean definitions something like...
For all sets $B$ and non-empty $A$, $f$ is a function mapping $A$ to $B$ iff
1) $f\subset A\times B$
2) $\forall x\in A: \exists y\in B: (x,y)\in f$
3) $\forall x,y_1,y_2:[ (x,y_1)\in f \land (x,y_2)\in f \implies y_1=y_2]$