:: deftheorem defines Group-like ABSRED_0:def 29 :
for S being non empty UAStr holds
( S is Group-like iff ( Seg 3 c= dom the charact of S & ( for f being non empty homogeneous PartFunc of ( the carrier of S *), the carrier of S holds
( ( f = the charact of S . 1 implies arity f = 0 ) & ( f = the charact of S . 2 implies arity f = 1 ) & ( f = the charact of S . 3 implies arity f = 2 ) ) ) ) );