:: deftheorem Def14 defines associative AOFA_000:def 14 :
for S being non empty UAStr holds
( S is associative iff the charact of S . 2 is non empty homogeneous quasi_total 2 -ary associative PartFunc of ( the carrier of S *), the carrier of S );