:: deftheorem Def2 defines $$ SETWOP_2:def 2 :
for D being non empty set
for p being FinSequence of D
for F being BinOp of D st ( F is having_a_unity or len p >= 1 ) & F is associative & F is commutative holds
F $$ p = F $$ ((findom p),([#] (p,(the_unity_wrt F))));