::
deftheorem
Def8
defines
.:^2
MONOID_1:def 8 :
for
D1
,
D2
,
D
being non
empty
set
for
f
being
Function
of
[:
D1
,
D2
:]
,
D
for
b
_{5}
being
Function
of
[:
(
bool
D1
)
,
(
bool
D2
)
:]
,
(
bool
D
)
holds
(
b
_{5}
=
f
.:^2
iff for
x
being
Element
of
[:
(
bool
D1
)
,
(
bool
D2
)
:]
holds
b
_{5}
.
x
=
f
.:
[:
(
x
`1
)
,
(
x
`2
)
:]
);