theorem Th12:
for
X,
Y,
D being non
empty set for
f being
Function of
X,
(Fin Y) for
g being
Function of
(Fin Y),
D for
F being
BinOp of
D st ( for
A,
B being
Element of
Fin Y st
A misses B holds
F . (
(g . A),
(g . B))
= g . (A \/ B) ) &
F is
commutative &
F is
associative &
F is
having_a_unity &
g . {} = the_unity_wrt F holds
for
I being
Element of
Fin X st ( for
x,
y being
object st
x in I &
y in I &
f . x meets f . y holds
x = y ) holds
(
F $$ (
I,
(g * f))
= F $$ (
(f .: I),
g) &
F $$ (
(f .: I),
g)
= g . (union (f .: I)) &
union (f .: I) is
Element of
Fin Y )