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?
EDIT
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]$
I honestly can't think of any literature off the top of my head with that restriction. Note that by allowing the empty set to be the domain of functions, you make the empty set an initial object in the category of sets.