:: deftheorem Def5 defines setopfunc BHSP_5:def 5 :
for DK, DX being non empty set
for f being BinOp of DK st f is commutative & f is associative & f is having_a_unity holds
for Y being finite Subset of DX
for F being Function of DX,DK
for b₆ being Element of DK holds
( b₆ = setopfunc (Y,DX,DK,F,f) iff ex p being FinSequence of DX st
( p is one-to-one & rng p = Y & b₆ = f "**" (Func_Seq (F,p)) ) );