:: deftheorem defines . MULTOP_1:def 2 :
for f being Function
for a, b, c, d being set holds f . (a,b,c,d) = f . [a,b,c,d];