:: deftheorem defines _ FLEXARY1:def 5 :
for o being Function-yielding Function
for x, y being object holds o _ (x,y) = (o . x) . y;