Definition function_equi
Definition.
function_equi
function f ↔ relation f ∧ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2
A
relation
f is called a
function
if for any position x there is at most one y such that (x, y) ∈ f.