for D being non empty set
for F being FinSequence of D
for g being BinOp of D st ( g is having_a_unity or len F >= 1 ) & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))