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)
X × Y → Z =: Op(X, Y, Z) viaf = (X × Y → Z(x, y) ↦ f((x, 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.