Library
▹
Essentials
▹
Operations
Definition 1.6.2.
Let
X
,
Y
,
Z
be sets,
∗
:
X
×
Y
→
Z
be an
operation
,
x
∈
X
,
y
∈
Y
. We define
x
∗
y
by:
x
(
X
×
Y
→
Z
(
a
,
b
)
↦
c
a
,
b
)
y
:
=
c
x
,
y
(
c
a
,
b
∈
Z
for each
a
∈
X
and
b
∈
Y
)
=
∗
((
x
,
y
))
Equality.
No proof.