:: 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);