Function

Definition

Function

A relation $f\subseteq A\times B$ is called function if every $a\in A$ is in relation to exactly one $b\in B$, i.e.,

$$\forall a\in A:\exists !b\in B:afb$$

where $\exists !$ denotes the counting quantifier.

Further, we write

$$f(a)=b⟺afb.$$