Definition. function_equi
function f ↔ relation f ∧ ∀x. ∀y1. ∀y2. (x, y1) ∈ f → (x, y2) ∈ f → y1 = y2