:: deftheorem Def2 defines associative AOFA_000:def 2 :
for f being homogeneous Function holds
( f is associative iff for x, y, z being set st <*x,y*> in dom f & <*y,z*> in dom f & <*(f . <*x,y*>),z*> in dom f & <*x,(f . <*y,z*>)*> in dom f holds
f . <*(f . <*x,y*>),z*> = f . <*x,(f . <*y,z*>)*> );