:: deftheorem defines . BINOP_1:def 1 :
for f being Function
for a, b being object holds f . (a,b) = f . [a,b];