theorem
:: MONOID_1:46
for
D1
,
D2
,
D
being non
empty
set
for
f
being
Function
of
[:
D1
,
D2
:]
,
D
for
X1
being
Subset
of
D1
for
X2
being
Subset
of
D2
holds
(
f
.:^2
)
.
(
X1
,
X2
)
=
{
(
f
.
(
a
,
b
)
)
where
a
is
Element
of
D1
,
b
is
Element
of
D2
: (
a
in
X1
&
b
in
X2
)
}