Definition 1.6.1. Let X, Y, Z be sets. We define:
Op(X, Y, Z) :=: {(X × Y → Z(x, y) ↦ zx,y) | zx,y ∈ Z for each x ∈ X and y ∈ Y}
(X × Y → Z(x, y) ↦ zx,y) = (X × Y → Z(x, y) ↦ z'x,y) :⇔ ∀ x ∈ X, y ∈ Y : zx,y = z'x,y (zx,y ∈ Z for each x ∈ X and y ∈ Y, z'x,y ∈ Z for each x ∈ X and y ∈ Y)
Well-definedness. No proof.
We write “let ∗ : X × Y → Z be an operation” for “let ∗ ∈ Op(X, Y, Z).”
We write “∗ : X × Y → Z(x, y) ↦ zx,y” for “∗ := (X × Y → Z(x, y) ↦ zx,y).”
References.