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 Y1, Y2 being finite Subset of DX st Y1 misses Y2 holds
for F being Function of DX,DK st Y1 c= dom F & Y2 c= dom F holds
for Z being finite Subset of DX st Z = Y1 \/ Y2 holds
setopfunc (Z,DX,DK,F,f) = f . ((setopfunc (Y1,DX,DK,F,f)),(setopfunc (Y2,DX,DK,F,f)))