Definition 1.5.2.  Let X, Y be sets, f:X → Y be a function, x ∈ X. We define
f(x)
by:
(X → Yz ↦ yz)(x) := yx  (yz ∈ Y for each z ∈ X)
Remarks.

This explicit definition works due to the special way that functions are defined. Within proofs, it enables unfolding of function application if the function has an explicit definition. The corresponding definition for mappings (see $../Relations/"mapping value") is an implicit definition instead.

References.