::
deftheorem
defines
..
MONOID_1:def 1 :
for
f
being
Function
for
x1
,
x2
,
y
being
set
holds
f
..
(
x1
,
x2
,
y
)
=
f
..
(
[
x1
,
x2
]
,
y
);