:: deftheorem defines ++ BHSP_5:def 1 :
for DX being non empty set
for f being BinOp of DX st f is commutative & f is associative & f is having_a_unity holds
for Y being finite Subset of DX
for b₄ being Element of DX holds
( b₄ = f ++ Y iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₄ = f "**" p ) );