Constant function formal definition A generic function $F : X \rightarrow Y$ can be defined as $\forall x \in X \exists !y \in Y (x, y) \in F$. How about the formal definition of a constant function? The formula $\exists !y \in Y \forall x \in X (x, y) \in F$ does not seem right to me, since it does not prevent that the same element in the set $X$ is mapped to multiple different elements in the set $Y$. Instead, it only prevents that two different constant lines can be mapped from the same set $X$.
How about just combining the two statements together?
$$(\forall x\in X\ \exists!y\in Y\ (x,y)\in F)\land(\exists y\in Y\ \forall x\in X\ (x,y)\in F)$$
Note that uniqueness of the $\exists$ in ths second statement is not required: suppose two such $y$'s existed, $y_1$ and $y_2$. Then for any element $x\in X$, $(x,y_1)$ and $(x,y_2)$ are in $F$, which is not allowed by the first statement. Thus only one such $y$ may exist.
Maybe $\exists! y \in Y : ((x,y) \in F , \forall x \in X) \land ((x,y') \notin F , \forall y' \ne y, \forall x \in X)$?