theorem
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)))